blob: 9f9eb3460e58860fe63ce52d6ea895223acaeba3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
|
