Makes the new row propagation system default (#2335)

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 7bfe8d59286a52c816a72b46fd15a319375df61e..80403ee0da89dc7aa5fbf28153ea4dd8da84a6bd 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -225,7 +225,7 @@ header = "options/arith_options.h"
   category   = "regular"
   long       = "new-prop"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use the new row propagation system"
 
 [[option]]

diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
index d7a0823040be46f4938e690cab352d413032dc5e..47006622dd2b6a3a5755d5135fdb4b4a4448752e 100644 (file)
--- a/test/regress/regress0/nl/ext-rew-aggr-test.smt2
+++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NIA)

diff --git a/test/regress/regress1/nl/metitarski-1025.smt2 b/test/regress/regress1/nl/metitarski-1025.smt2
index 5a95364f3567fc1342b3d9b2de4985190bde3e3f..73a132350cdec49f74bdce4d662bea461b362dd9 100644 (file)
--- a/test/regress/regress1/nl/metitarski-1025.smt2
+++ b/test/regress/regress1/nl/metitarski-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext --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 835d60732625d6c0f31ab0e57bc3aee613c7e700..3a1e794cc8b29b251e09568bd979c9a8e0e499a2 100644 (file)
--- 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
+; COMMAND-LINE: --nl-ext --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |