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