--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on May 2009 ---
-smt-solver only useful for choosing solver for .smt files. When a .why file is given to why-dp, it necessarily calls alt-ergo. - Claude St?phane DUPRAT wrote: > Hi Claude, > > I want to force the use of alt-ergo and if I try with the id "alt-ergo" > I have an error : > > $ why-dp -smt-solver alt-ergo fic.why > unknown SMT solver alt-ergo > > How can I be sure that alt-ergo if really called if Idon't use de > -smt-solver option ? > > thanks, > > St?phane > > > > > Claude March? a ?crit : >> 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 |