diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-15 00:15:49 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-15 00:15:49 +0000 |
| commit | d9c6de378604c96d82a0e74bb4da497d8e205d0a (patch) | |
| tree | 144a67a30e322d2242dafb640f38e9cd19d21c2f /test | |
| parent | 1302e3fb1ffdbed229112106932488e3fff6810c (diff) | |
one bug fixed
Diffstat (limited to 'test')
| -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])) |