diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-02 12:15:48 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-02 10:15:48 -0700 |
| commit | 806f4071423ee1bf8f02f1836843de73faabb952 (patch) | |
| tree | c50e9261633d5e31a7beb3b4a7f20b10ddcd641d /test/regress | |
| parent | e0e63f746fb0f022fa6594dcc701a2d881155f9b (diff) | |
Fix preinitialization pass for finite model finding (#2047)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/Makefile.tests | 3 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue2034-preinit.smt2 | 8 |
2 files changed, 10 insertions, 1 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index d235f27d3..0e0cee7f8 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1085,6 +1085,7 @@ REG1_TESTS = \ regress1/fmf/german169.smt2 \ regress1/fmf/german73.smt2 \ regress1/fmf/issue916-fmf-or.smt2 \ + regress1/fmf/issue2034-preinit.smt2 \ regress1/fmf/jasmin-cdt-crash.smt2 \ regress1/fmf/ko-bound-set.cvc \ regress1/fmf/loopy_coda.smt2 \ @@ -1589,7 +1590,6 @@ REG2_TESTS = \ regress2/ooo.tag10.smt2 \ regress2/piVC_5581bd.smt2 \ regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \ - regress2/quantifiers/ForElimination-scala-9.smt2 \ regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \ regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \ regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \ @@ -1958,6 +1958,7 @@ DISABLED_TESTS = \ regress2/bug396.smt2 \ regress2/nl/dumortier-050317.smt2 \ regress2/nl/nt-lemmas-bad.smt2 \ + regress2/quantifiers/ForElimination-scala-9.smt2 \ regress2/quantifiers/small-bug1-fixpoint-3.smt2 \ regress2/xs-11-20-5-2-5-3.smt \ regress2/xs-11-20-5-2-5-3.smt2 diff --git a/test/regress/regress1/fmf/issue2034-preinit.smt2 b/test/regress/regress1/fmf/issue2034-preinit.smt2 new file mode 100644 index 000000000..e80e698fd --- /dev/null +++ b/test/regress/regress1/fmf/issue2034-preinit.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unknown +(set-logic AUFLIRA) +(set-info :status unknown) +(declare-fun _substvar_1_ () Int) +(declare-fun tptp_const_array1 (Int Real) (Array Int Real)) +(assert (forall ((?I_4 Int) (?L_5 Int) (?U_6 Int) (?Val_7 Real)) (=> true (= (select (tptp_const_array1 _substvar_1_ ?Val_7) 0) ?Val_7)))) +(check-sat)
\ No newline at end of file |