diff options
Diffstat (limited to 'test/regress/regress0')
27 files changed, 27 insertions, 27 deletions
diff --git a/test/regress/regress0/nl/bug698.smt2 b/test/regress/regress0/nl/bug698.smt2 index ba7610145..ffb1eead2 100644 --- a/test/regress/regress0/nl/bug698.smt2 +++ b/test/regress/regress0/nl/bug698.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --nl-alg --fmf-fun-rlv --no-check-models +; COMMAND-LINE: --incremental --nl-ext --fmf-fun-rlv --no-check-models (set-logic UFNIA) (set-info :smt-lib-version 2.5) diff --git a/test/regress/regress0/nl/coeff-sat.smt2 b/test/regress/regress0/nl/coeff-sat.smt2 index 08d189af1..84502bb63 100644 --- a/test/regress/regress0/nl/coeff-sat.smt2 +++ b/test/regress/regress0/nl/coeff-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/coeff-unsat-base.smt2 b/test/regress/regress0/nl/coeff-unsat-base.smt2 index e91cae09e..d56421bf9 100644 --- a/test/regress/regress0/nl/coeff-unsat-base.smt2 +++ b/test/regress/regress0/nl/coeff-unsat-base.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/coeff-unsat.smt2 b/test/regress/regress0/nl/coeff-unsat.smt2 index 91e4506da..f86d08fe7 100644 --- a/test/regress/regress0/nl/coeff-unsat.smt2 +++ b/test/regress/regress0/nl/coeff-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/combine.smt2 b/test/regress/regress0/nl/combine.smt2 index 9c9d839d4..9f7e7a548 100644 --- a/test/regress/regress0/nl/combine.smt2 +++ b/test/regress/regress0/nl/combine.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/disj-eval.smt2 b/test/regress/regress0/nl/disj-eval.smt2 index 717f7a28f..ac8cfc937 100644 --- a/test/regress/regress0/nl/disj-eval.smt2 +++ b/test/regress/regress0/nl/disj-eval.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) diff --git a/test/regress/regress0/nl/dist-big.smt2 b/test/regress/regress0/nl/dist-big.smt2 index cbd87b085..53c9c3f1d 100644 --- a/test/regress/regress0/nl/dist-big.smt2 +++ b/test/regress/regress0/nl/dist-big.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 index d0c038d73..9411224e5 100644 --- a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 +++ b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski-1025.smt2 b/test/regress/regress0/nl/metitarski-1025.smt2 index af922a466..5a95364f3 100644 --- a/test/regress/regress0/nl/metitarski-1025.smt2 +++ b/test/regress/regress0/nl/metitarski-1025.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski-3-4.smt2 b/test/regress/regress0/nl/metitarski-3-4.smt2 index 2cd913379..835d60732 100644 --- a/test/regress/regress0/nl/metitarski-3-4.smt2 +++ b/test/regress/regress0/nl/metitarski-3-4.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski_3_4_2e.smt2 b/test/regress/regress0/nl/metitarski_3_4_2e.smt2 index d08aef410..3f12ec34b 100644 --- a/test/regress/regress0/nl/metitarski_3_4_2e.smt2 +++ b/test/regress/regress0/nl/metitarski_3_4_2e.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/mult-po.smt2 b/test/regress/regress0/nl/mult-po.smt2 index 3f38a7236..65498338a 100644 --- a/test/regress/regress0/nl/mult-po.smt2 +++ b/test/regress/regress0/nl/mult-po.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/nia-wrong-tl.smt2 b/test/regress/regress0/nl/nia-wrong-tl.smt2 index 25cae599b..40ac92b43 100644 --- a/test/regress/regress0/nl/nia-wrong-tl.smt2 +++ b/test/regress/regress0/nl/nia-wrong-tl.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) diff --git a/test/regress/regress0/nl/nl-help-unsat-quant.smt2 b/test/regress/regress0/nl/nl-help-unsat-quant.smt2 index 45a504de3..f2f7667c8 100644 --- a/test/regress/regress0/nl/nl-help-unsat-quant.smt2 +++ b/test/regress/regress0/nl/nl-help-unsat-quant.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/nl-unk-quant.smt2 b/test/regress/regress0/nl/nl-unk-quant.smt2 index 4ab034c7c..bb5cd43df 100644 --- a/test/regress/regress0/nl/nl-unk-quant.smt2 +++ b/test/regress/regress0/nl/nl-unk-quant.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) diff --git a/test/regress/regress0/nl/nt-lemmas-bad.smt2 b/test/regress/regress0/nl/nt-lemmas-bad.smt2 index c137214f6..cea877c23 100644 --- a/test/regress/regress0/nl/nt-lemmas-bad.smt2 +++ b/test/regress/regress0/nl/nt-lemmas-bad.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg --nl-alg-tplanes +; COMMAND-LINE: --nl-ext --nl-ext-tplanes ; EXPECT: unsat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/ones.smt2 b/test/regress/regress0/nl/ones.smt2 index 88e73c56e..be06912d0 100644 --- a/test/regress/regress0/nl/ones.smt2 +++ b/test/regress/regress0/nl/ones.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/poly-1025.smt2 b/test/regress/regress0/nl/poly-1025.smt2 index 0a6e9dcf3..482696532 100644 --- a/test/regress/regress0/nl/poly-1025.smt2 +++ b/test/regress/regress0/nl/poly-1025.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/quant-nl.smt2 b/test/regress/regress0/nl/quant-nl.smt2 index 2544a5f2e..7d251ab7d 100644 --- a/test/regress/regress0/nl/quant-nl.smt2 +++ b/test/regress/regress0/nl/quant-nl.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/red-exp.smt2 b/test/regress/regress0/nl/red-exp.smt2 index 9a413902d..5dc5258e2 100644 --- a/test/regress/regress0/nl/red-exp.smt2 +++ b/test/regress/regress0/nl/red-exp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/rewriting-sums.smt2 b/test/regress/regress0/nl/rewriting-sums.smt2 index 9d0f33e9f..ca2edf024 100644 --- a/test/regress/regress0/nl/rewriting-sums.smt2 +++ b/test/regress/regress0/nl/rewriting-sums.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/simple-mono-unsat.smt2 b/test/regress/regress0/nl/simple-mono-unsat.smt2 index e640c943b..b82b7ad7c 100644 --- a/test/regress/regress0/nl/simple-mono-unsat.smt2 +++ b/test/regress/regress0/nl/simple-mono-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/simple-mono.smt2 b/test/regress/regress0/nl/simple-mono.smt2 index a9761fa5a..3d4adad28 100644 --- a/test/regress/regress0/nl/simple-mono.smt2 +++ b/test/regress/regress0/nl/simple-mono.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/subs0-unsat-confirm.smt2 b/test/regress/regress0/nl/subs0-unsat-confirm.smt2 index 044f7654c..a1df91b17 100644 --- a/test/regress/regress0/nl/subs0-unsat-confirm.smt2 +++ b/test/regress/regress0/nl/subs0-unsat-confirm.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/very-easy-sat.smt2 b/test/regress/regress0/nl/very-easy-sat.smt2 index b9aecac7a..06efa5806 100644 --- a/test/regress/regress0/nl/very-easy-sat.smt2 +++ b/test/regress/regress0/nl/very-easy-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/very-simple-unsat.smt2 b/test/regress/regress0/nl/very-simple-unsat.smt2 index bcfdaad40..e23d2d542 100644 --- a/test/regress/regress0/nl/very-simple-unsat.smt2 +++ b/test/regress/regress0/nl/very-simple-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/zero-subset.smt2 b/test/regress/regress0/nl/zero-subset.smt2 index 6087551c1..a8ce65b02 100644 --- a/test/regress/regress0/nl/zero-subset.smt2 +++ b/test/regress/regress0/nl/zero-subset.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) |