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

[Frama-c-discuss] using different versions of z3



Christoph Weber wrote:
> Hello,
>
> I would like to thank you for your answers on my previous questions.
>
> As I am trying to adapt examples to the new features of Frama-c, I have
> discovered that the smt-solver z3 has been updated as well.
>
> Unfortunatly, the results of z3 v1.3 and z3 v2.1 differ a lot. Since I do
> not know what internal changes may cause this difference, I would like to
> run both z3 versions simultaneously.
>
> I would like to have a description, on how to recognize both with
> why-config.
>   
Why is not designed to support several versions of the same prover. 
However, you can fool it by a simple hack:

call z3 2.1 executable as "z3"
call z3 1.3 as "yices"
call another smt prover as "cvc3"

- Claude


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