1 files changed, 29 insertions, 0 deletions
diff --git a/matthew_test.sh b/matthew_test.sh
new file mode 100755
index 000000000..9f9eb3460
--- /dev/null
+++ b/matthew_test.sh
@@ -0,0 +1,29 @@
+#!/bin/bash
+
+set -e
+
+RUN_SIMPLE=false
+GET_STATS=true
+RUN_SMTLIB=500
+TIMEOUT_SMTLIB=5m
+
+if [ $GET_STATS = true ] ; then
+  OPTS="$OPTS --stats-expert"
+fi
+
+OPTS="$OPTS --arith-idl-ext"
+
+if [ $RUN_SIMPLE = true ] ; then
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example-rewritten.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/example-rewritten-sat.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/matthew-many-syntax.smt2
+  ./bin/cvc5 --arith-idl-ext ../test/regress/regress0/idl/matthew-backtrack-needed.smt2
+fi
+# ./bin/cvc5 --stats-expert --arith-idl-ext ../test/regress/regress0/idl/matthew-adapted-smtlib.smt2
+
+for test_file in $(cat $HOME/sorted_smt_lib.list | head -n $RUN_SMTLIB)
+do
+  echo "./bin/cvc5 $OPTS $test_file"
+  timeout $TIMEOUT_SMTLIB ./bin/cvc5 $OPTS $test_file
+done