diff --git a/scripts/test-solvers b/scripts/test-solvers new file mode 100755 index 0000000000000000000000000000000000000000..058d9069ad5d9cb2e88eeb46a32150aa14862234 --- /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}"