Merge branch 'master' into fixWinBuildfixWinBuild

35 files changed, 35 insertions, 35 deletions

diff --git a/test/regress/regress1/nl/arrowsmith-050317.smt2 b/test/regress/regress1/nl/arrowsmith-050317.smt2
index e24df9d23..762d617ad 100644
--- a/test/regress/regress1/nl/arrowsmith-050317.smt2
+++ b/test/regress/regress1/nl/arrowsmith-050317.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/bad-050217.smt2 b/test/regress/regress1/nl/bad-050217.smt2
index 69a033001..4f3cf8951 100644
--- a/test/regress/regress1/nl/bad-050217.smt2
+++ b/test/regress/regress1/nl/bad-050217.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRAT)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/bug698.smt2 b/test/regress/regress1/nl/bug698.smt2
index f24d05372..221a5613d 100644
--- a/test/regress/regress1/nl/bug698.smt2
+++ b/test/regress/regress1/nl/bug698.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --nl-ext --fmf-fun-rlv --no-check-models
+; COMMAND-LINE: --incremental --nl-ext=full --fmf-fun-rlv --no-check-models
 (set-logic UFNIA)
 (set-info :smt-lib-version 2.6)
 
diff --git a/test/regress/regress1/nl/coeff-unsat-base.smt2 b/test/regress/regress1/nl/coeff-unsat-base.smt2
index d56421bf9..97c8fa375 100644
--- a/test/regress/regress1/nl/coeff-unsat-base.smt2
+++ b/test/regress/regress1/nl/coeff-unsat-base.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/coeff-unsat.smt2 b/test/regress/regress1/nl/coeff-unsat.smt2
index f86d08fe7..2e32906f2 100644
--- a/test/regress/regress1/nl/coeff-unsat.smt2
+++ b/test/regress/regress1/nl/coeff-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/combine.smt2 b/test/regress/regress1/nl/combine.smt2
index 9f7e7a548..94bdc8027 100644
--- a/test/regress/regress1/nl/combine.smt2
+++ b/test/regress/regress1/nl/combine.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/cos-bound.smt2 b/test/regress/regress1/nl/cos-bound.smt2
index d5052f675..1371a33c7 100644
--- a/test/regress/regress1/nl/cos-bound.smt2
+++ b/test/regress/regress1/nl/cos-bound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (declare-fun x () Real)
diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2
index 4b911e576..bedc0209b 100644
--- a/test/regress/regress1/nl/cos1-tc.smt2
+++ b/test/regress/regress1/nl/cos1-tc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
+; COMMAND-LINE: --nl-ext=full --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
 ; EXPECT: unknown
 (set-logic UFNRAT)
 (declare-fun f (Real) Real)
diff --git a/test/regress/regress1/nl/disj-eval.smt2 b/test/regress/regress1/nl/disj-eval.smt2
index ac8cfc937..e8287ab0f 100644
--- a/test/regress/regress1/nl/disj-eval.smt2
+++ b/test/regress/regress1/nl/disj-eval.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/dist-big.smt2 b/test/regress/regress1/nl/dist-big.smt2
index 53c9c3f1d..e73a5bc68 100644
--- a/test/regress/regress1/nl/dist-big.smt2
+++ b/test/regress/regress1/nl/dist-big.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/div-mod-partial.smt2 b/test/regress/regress1/nl/div-mod-partial.smt2
index c94acf770..0f0d60fa9 100644
--- a/test/regress/regress1/nl/div-mod-partial.smt2
+++ b/test/regress/regress1/nl/div-mod-partial.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes -q
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes -q
 ; EXPECT: sat
 (set-logic QF_UFNIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/exp-soundness-bound.smt2 b/test/regress/regress1/nl/exp-soundness-bound.smt2
index 5bcae30b0..8074fb2f2 100644
--- a/test/regress/regress1/nl/exp-soundness-bound.smt2
+++ b/test/regress/regress1/nl/exp-soundness-bound.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --decision=internal --no-check-models
+; COMMAND-LINE: --nl-ext=full --decision=internal --no-check-models
 ; EXPECT: sat
 (set-logic ALL)
 (assert (or (< 60.3 (exp 4.1) 60.4) (< (exp 5.1) 164.1)))
diff --git a/test/regress/regress1/nl/exp_monotone.smt2 b/test/regress/regress1/nl/exp_monotone.smt2
index 0d754dada..74f646534 100644
--- a/test/regress/regress1/nl/exp_monotone.smt2
+++ b/test/regress/regress1/nl/exp_monotone.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/metitarski-1025.smt2 b/test/regress/regress1/nl/metitarski-1025.smt2
index 3fbf9cb77..200d5903e 100644
--- a/test/regress/regress1/nl/metitarski-1025.smt2
+++ b/test/regress/regress1/nl/metitarski-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-new-prop
+; COMMAND-LINE: --nl-ext=full --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |
diff --git a/test/regress/regress1/nl/metitarski-3-4.smt2 b/test/regress/regress1/nl/metitarski-3-4.smt2
index f26640f49..9ed273be6 100644
--- a/test/regress/regress1/nl/metitarski-3-4.smt2
+++ b/test/regress/regress1/nl/metitarski-3-4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-new-prop
+; COMMAND-LINE: --nl-ext=full --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |
diff --git a/test/regress/regress1/nl/metitarski_3_4_2e.smt2 b/test/regress/regress1/nl/metitarski_3_4_2e.smt2
index 07efc3d32..7771dcaad 100644
--- a/test/regress/regress1/nl/metitarski_3_4_2e.smt2
+++ b/test/regress/regress1/nl/metitarski_3_4_2e.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2
index 0b341ac6a..9598c8477 100644
--- a/test/regress/regress1/nl/mirko-050417.smt2
+++ b/test/regress/regress1/nl/mirko-050417.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/nl-help-unsat-quant.smt2 b/test/regress/regress1/nl/nl-help-unsat-quant.smt2
index d0acca99d..f32cd1927 100644
--- a/test/regress/regress1/nl/nl-help-unsat-quant.smt2
+++ b/test/regress/regress1/nl/nl-help-unsat-quant.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic UFNIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/nl-unk-quant.smt2 b/test/regress/regress1/nl/nl-unk-quant.smt2
index 64cc419d7..253811bcb 100644
--- a/test/regress/regress1/nl/nl-unk-quant.smt2
+++ b/test/regress/regress1/nl/nl-unk-quant.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; 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/regress1/nl/ones.smt2 b/test/regress/regress1/nl/ones.smt2
index be06912d0..79ecebb57 100644
--- a/test/regress/regress1/nl/ones.smt2
+++ b/test/regress/regress1/nl/ones.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/poly-1025.smt2 b/test/regress/regress1/nl/poly-1025.smt2
index 2fb918e3c..6459f29bf 100644
--- a/test/regress/regress1/nl/poly-1025.smt2
+++ b/test/regress/regress1/nl/poly-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |
diff --git a/test/regress/regress1/nl/quant-nl.smt2 b/test/regress/regress1/nl/quant-nl.smt2
index f47023e99..f2f3f83d2 100644
--- a/test/regress/regress1/nl/quant-nl.smt2
+++ b/test/regress/regress1/nl/quant-nl.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic UFNIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/red-exp.smt2 b/test/regress/regress1/nl/red-exp.smt2
index 5dc5258e2..95e6efb80 100644
--- a/test/regress/regress1/nl/red-exp.smt2
+++ b/test/regress/regress1/nl/red-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/rewriting-sums.smt2 b/test/regress/regress1/nl/rewriting-sums.smt2
index ca2edf024..74c38c841 100644
--- a/test/regress/regress1/nl/rewriting-sums.smt2
+++ b/test/regress/regress1/nl/rewriting-sums.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/shifting.smt2 b/test/regress/regress1/nl/shifting.smt2
index 320c92d58..e460532ae 100644
--- a/test/regress/regress1/nl/shifting.smt2
+++ b/test/regress/regress1/nl/shifting.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: sat
 (set-logic QF_NIRA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/shifting2.smt2 b/test/regress/regress1/nl/shifting2.smt2
index c5e805c50..9122701f6 100644
--- a/test/regress/regress1/nl/shifting2.smt2
+++ b/test/regress/regress1/nl/shifting2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NIRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/simple-mono-unsat.smt2 b/test/regress/regress1/nl/simple-mono-unsat.smt2
index b82b7ad7c..5e5446382 100644
--- a/test/regress/regress1/nl/simple-mono-unsat.smt2
+++ b/test/regress/regress1/nl/simple-mono-unsat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/simple-mono.smt2 b/test/regress/regress1/nl/simple-mono.smt2
index 3d4adad28..092d9e90e 100644
--- a/test/regress/regress1/nl/simple-mono.smt2
+++ b/test/regress/regress1/nl/simple-mono.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/sin-compare-across-phase.smt2 b/test/regress/regress1/nl/sin-compare-across-phase.smt2
index c4c28f527..9c700b891 100644
--- a/test/regress/regress1/nl/sin-compare-across-phase.smt2
+++ b/test/regress/regress1/nl/sin-compare-across-phase.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/sin-compare.smt2 b/test/regress/regress1/nl/sin-compare.smt2
index d22cec0b9..a65220744 100644
--- a/test/regress/regress1/nl/sin-compare.smt2
+++ b/test/regress/regress1/nl/sin-compare.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/sin-init-tangents.smt2 b/test/regress/regress1/nl/sin-init-tangents.smt2
index fa29cd911..bf8cf9134 100644
--- a/test/regress/regress1/nl/sin-init-tangents.smt2
+++ b/test/regress/regress1/nl/sin-init-tangents.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/sin-sign.smt2 b/test/regress/regress1/nl/sin-sign.smt2
index df2a56b32..7da92ae53 100644
--- a/test/regress/regress1/nl/sin-sign.smt2
+++ b/test/regress/regress1/nl/sin-sign.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/sin-sym2.smt2 b/test/regress/regress1/nl/sin-sym2.smt2
index 45d86dcac..eb47f113d 100644
--- a/test/regress/regress1/nl/sin-sym2.smt2
+++ b/test/regress/regress1/nl/sin-sym2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --nl-ext-tplanes
+; COMMAND-LINE: --nl-ext=full --nl-ext-tplanes
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/tan-rewrite2.smt2 b/test/regress/regress1/nl/tan-rewrite2.smt2
index 601021a7f..4e3b1f7e8 100644
--- a/test/regress/regress1/nl/tan-rewrite2.smt2
+++ b/test/regress/regress1/nl/tan-rewrite2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_UFNRAT)
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/zero-subset.smt2 b/test/regress/regress1/nl/zero-subset.smt2
index a8ce65b02..1df45f2d2 100644
--- a/test/regress/regress1/nl/zero-subset.smt2
+++ b/test/regress/regress1/nl/zero-subset.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext=full
 ; EXPECT: unsat
 (set-logic QF_NRA)
 (set-info :status unsat)