Commit 8d3da38a authored by David Hauzar's avatar David Hauzar
Browse files

Update to driver for cvc4 for getting model.

parent cc774eb2
......@@ -13,6 +13,14 @@ prelude "(set-logic AUFNIRA)"
prelude ";; Enable model construction"
prelude "(set-option :produce-models true)"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_intro" *)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
transformation "introduce_premises"
import "smt-libv2.drv"
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
(* transformation "split_goal_wp" *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment