Commit 303cab0f authored by David Hauzar's avatar David Hauzar
Browse files

Bugfix: driver for cvc4 (bugs inserted when resolving merge conflict when...

Bugfix: driver for cvc4 (bugs inserted when resolving merge conflict when rebasing the master branch).
parent 47161a48
......@@ -19,22 +19,6 @@ prelude "(set-option :produce-models true)"
(* 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_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" *)
(* Counterexamples: get rid of some quantifiers - makes it possible to query model values of the variables in premises *)
transformation "introduce_premises"
(* Counterexamples: set model parser *)
model_parser "cvc4_z3"
......
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