diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/decision/Makefile.am | 7 | ||||
| -rw-r--r-- | test/regress/regress0/decision/error3.delta01.smt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/decision/error3.smt | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 31f54fdfc..f40a65161 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -27,10 +27,11 @@ TESTS = \ error20.smt \ error20.delta01.smt \ error122.smt \ - error122.delta01.smt + error122.delta01.smt \ + error3.smt \ + error3.delta01.smt + # Incorrect answers: -# error3.smt \ -# error3.delta01.smt # EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/decision/error3.delta01.smt b/test/regress/regress0/decision/error3.delta01.smt index 59568bad6..de4bccd77 100644 --- a/test/regress/regress0/decision/error3.delta01.smt +++ b/test/regress/regress0/decision/error3.delta01.smt @@ -2,7 +2,7 @@ :logic QF_AUFBV :extrafuns ((v1 BitVec[3])) :extrafuns ((a2 Array[13:3])) -:status unknown +:status unsat :formula (let (?n1 bv0[3]) (flet ($n2 (bvsgt v1 v1)) diff --git a/test/regress/regress0/decision/error3.smt b/test/regress/regress0/decision/error3.smt index 57a982d08..36c409f3f 100644 --- a/test/regress/regress0/decision/error3.smt +++ b/test/regress/regress0/decision/error3.smt @@ -1,6 +1,6 @@ (benchmark fuzzsmt :logic QF_AUFBV -:status unknown +:status unsat :extrafuns ((v0 BitVec[15])) :extrafuns ((v1 BitVec[3])) :extrafuns ((a2 Array[13:3])) |