--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on May 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] usage of why-dp



it is an id, either "yices", "cvc3" or "z3"

Sorry for the poor documentation

- Claude

St?phane DUPRAT wrote:
> Hi,
> 
> why-dp encapsulates calls of the solvers, but wich solver is called ?
> Does it depends on the suffix of the obligation file (ex: alt-ergo for 
> .why file) ?
> I've seen the -smt-solver <solver> option, but what is "solver" : a 
> command line or an id ?
> 
> regards,
> 
> St?phane
> 
> 
> 

-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |