--- layout: fc_discuss_archives title: Message 35 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



-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                    |