blob: 94e80b940c691db13a15239f8068cb8c5c30573c (
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
cvc4=./cvc4
bench="$1"
logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic *\([A-Z_]*\) *) *$')
case "$logic" in
QF_BV)
# run tear-down incremental
#
# we run in this way for line-buffered input, otherwise memory's a
# concern (plus it mimics what we'll end up getting from an
# application-track trace runner?)
cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --tear-down-incremental
;;
*)
# just run the default --incremental
#
# we run in this way for line-buffered input, otherwise memory's a
# concern (plus it mimics what we'll end up getting from an
# application-track trace runner?)
cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --incremental
;;
esac
|
