diff options
Diffstat (limited to 'test/regress/regress0/uflia')
| -rw-r--r-- | test/regress/regress0/uflia/Makefile.am | 8 | ||||
| -rw-r--r-- | test/regress/regress0/uflia/microwave21.ec.minimized.smt2 | 4 |
2 files changed, 5 insertions, 7 deletions
diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 751d69fe5..27487b962 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -40,15 +40,13 @@ SMT2_TESTS = \ FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \ stalmark_e7_27_e7_31.ec.minimized.smt2 \ stalmark_e7_27_e7_31.ec.smt2 \ - tiny.smt2 + tiny.smt2 \ + speed2_e8_449_e8_517.ec.smt2 \ + microwave21.ec.minimized.smt2 # simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 # javafe.ast.StandardPrettyPrint.319_no_forall.smt2 # javafe.ast.WhileStmt.447_no_forall.smt2 -# CURRENTLY FAILING: -# speed2_e8_449_e8_517.ec.smt2 -# microwave21.ec.minimized.smt2 - # Regression tests for PL inputs CVC_TESTS = diff --git a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 index 0d9accb91..b37db9a1e 100644 --- a/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 +++ b/test/regress/regress0/uflia/microwave21.ec.minimized.smt2 @@ -1,7 +1,7 @@ ; initialize_defs ; PROPERTY DEFGEN (set-logic QF_UFNIA) -(set-info :status sat) +(set-info :status unsat) (declare-fun _base () Int) (declare-fun _n () Int) (assert (>= _n 0)) @@ -441,4 +441,4 @@ ; not refinement_pass (assert (not (=> (= _base (- 0 1)) (and (P (- 0 1)) (P 0))))) (assert true) -(check-sat)
\ No newline at end of file +(check-sat) |