--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on May 2009 ---
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 |