summaryrefslogtreecommitdiff
path: root/contrib/cvc4_strict_smtlib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/cvc4_strict_smtlib')
-rw-r--r--contrib/cvc4_strict_smtlib8
1 files changed, 8 insertions, 0 deletions
diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib
new file mode 100644
index 000000000..0a97bd74b
--- /dev/null
+++ b/contrib/cvc4_strict_smtlib
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+cvc4="${CVC4_HOME}/cvc4"
+
+# This is the set of command line arguments that is required to be strictly
+# complaint with the input and output requirements of the current SMT-LIB
+# standard.
+"$cvc4" --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values $@
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback