--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Why3-club] why3-0.88.0 and CVC4 1.4/1.5



it is

why3 prove -P CVC4,1.5 ...

sorry for the confusion between -P and -D

- Claude


Le 24/10/2017 à 16:10, Gerlach, Jens a écrit :
> Hello Claude, 
> 
> I tried your suggestion on one of our examples 
> 	why3 prove -D CVC4,1.5 find_assert_rte_mem_access_Alt-Ergo.mlw
> and received the following error message
> 	anomaly: Sys_error("CVC4,1.5: No such file or directory")
> 
> When I try
> 	why3 prove -D CVC4 find_assert_rte_mem_access_Alt-Ergo.mlw
> the error message is a bit more specific
> 	anomaly: Sys_error("/home/jens/.opam/system/share/why3/drivers/CVC4.drv: No such file or directory")
> 
> In  ~/.opam/system/share/why3/drivers/ there are
> 
> 	cvc4_14.drv
> 	cvc4_15.drv
> 	cvc4_bv.gen
> 	cvc4.drv
> 	cvc4-realize.drv
> 
> Regards
> 
> Jens
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> 

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - ÃŽle-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |