diff options
Diffstat (limited to 'test/regress/regress0/uflia')
10 files changed, 20 insertions, 15 deletions
diff --git a/test/regress/regress0/uflia/check02.smt2 b/test/regress/regress0/uflia/check02.smt2 index 0920170c6..daa3ca417 100644 --- a/test/regress/regress0/uflia/check02.smt2 +++ b/test/regress/regress0/uflia/check02.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun b () Int) (declare-fun n () Int) diff --git a/test/regress/regress0/uflia/check02.smt2.expect b/test/regress/regress0/uflia/check02.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check02.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/check03.smt2 b/test/regress/regress0/uflia/check03.smt2 index f561e1964..e4503ba1d 100644 --- a/test/regress/regress0/uflia/check03.smt2 +++ b/test/regress/regress0/uflia/check03.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/check03.smt2.expect b/test/regress/regress0/uflia/check03.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check03.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/check04.smt2 b/test/regress/regress0/uflia/check04.smt2 index 61bc8a5d6..a6630dfa3 100644 --- a/test/regress/regress0/uflia/check04.smt2 +++ b/test/regress/regress0/uflia/check04.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_LIA) (declare-fun _b () Int) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/check04.smt2.expect b/test/regress/regress0/uflia/check04.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/check04.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 index 019d70de9..779b6237b 100644 --- a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 +++ b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun _base () Int) (declare-fun _n () Int) diff --git a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect b/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect deleted file mode 100644 index fe118171a..000000000 --- a/test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental -% EXPECT: sat -% EXPECT: unsat diff --git a/test/regress/regress0/uflia/tiny.smt2 b/test/regress/regress0/uflia/tiny.smt2 index fc0251a55..bad1964c2 100644 --- a/test/regress/regress0/uflia/tiny.smt2 +++ b/test/regress/regress0/uflia/tiny.smt2 @@ -1,3 +1,7 @@ +; COMMAND-LINE: --incremental --simplification=none +; EXPECT: sat +; EXPECT: unsat + (set-logic QF_UFLIA) (declare-fun base () Int) (declare-fun n () Int) diff --git a/test/regress/regress0/uflia/tiny.smt2.expect b/test/regress/regress0/uflia/tiny.smt2.expect deleted file mode 100644 index 7081f83db..000000000 --- a/test/regress/regress0/uflia/tiny.smt2.expect +++ /dev/null @@ -1,3 +0,0 @@ -% COMMAND-LINE: --incremental --simplification=none -% EXPECT: sat -% EXPECT: unsat |