From 2540be1197de2a60c474400c9d94b8a7b6f24a1b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Mon, 20 Oct 2014 17:53:01 +0200
Subject: [PATCH] Add script for testing solvers
---
scripts/test-solvers | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
create mode 100755 scripts/test-solvers
diff --git a/scripts/test-solvers b/scripts/test-solvers
new file mode 100755
index 000000000..058d9069a
--- /dev/null
+++ b/scripts/test-solvers
@@ -0,0 +1,20 @@
+#!/bin/bash
+
+echo "Running Z3:"
+T="$(date +%s)"
+for f in vcs/z3*; do
+ z3 -in -smt2 < $f > /dev/null
+done
+T="$(($(date +%s)-T))"
+echo "Time in seconds: ${T}"
+
+
+echo "Testing CVC4"
+T="$(date +%s)"
+for f in vcs/cvc4*; do
+ #cvc4-master -q --produce-models --no-incremental --tear-down-incremental --dt-rewrite-error-sel --print-success --lang smt < $f > /dev/null
+ #cvc4-master -q --dt-binary-split --produce-models --incremental --dt-rewrite-error-sel --print-success --lang smt < $f
+ cvc4-master -q --decision=internal --produce-models --incremental --dt-rewrite-error-sel --print-success --lang smt < $f
+done
+T="$(($(date +%s)-T))"
+echo "Time in seconds: ${T}"
--
GitLab