Commit 6f584eaa authored by David Hauzar's avatar David Hauzar

Update to driver for cvc4 for getting model.

parent cfa0b420
prelude "(set-logic ALL_SUPPORTED)"
prelude "(set-logic AUFNIRA)"
(* cvc4 does not support generating counterexamples with non-linear arithmetic *)
(* prelude "(set-logic AUFLIRA)" *)
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
......@@ -7,6 +9,16 @@ prelude "(set-logic ALL_SUPPORTED)"
*)
(* prelude "(set-logic ALL_SUPPORTED)" *)
(* Counterexamples: enable model construction *)
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"
(* regexp for steps *)
......
Markdown is supported
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