--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on October 2017 ---
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 |