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



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