Disable ordering heuristic for justification by default (#6848)

diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 840eaa08fd7db9b01d913961708bd589d33568c0..8cc2bf2fe568aedb891ad2d48be6636927f586cf 100644 (file)
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -92,7 +92,7 @@ name   = "Decision Heuristics"
   category   = "expert"
   long       = "jh-rlv-order"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "maintain activity-based ordering for decision justification heuristic"
 
 [[option]]

diff --git a/test/regress/regress1/rels/bv1p.cvc b/test/regress/regress1/rels/bv1p.cvc
index 0e8803ce64656d0a07414e4527b783a96a1defa6..ed9fdce1f3512b28f0433c95f3ae17df572cad22 100644 (file)
--- a/test/regress/regress1/rels/bv1p.cvc
+++ b/test/regress/regress1/rels/bv1p.cvc
@@ -1,4 +1,8 @@
+% COMMAND-LINE: --jh-rlv-order
 % EXPECT: unsat
+
+% note we require jh-rlv-order on this benchmark to avoid a proof failure currently (7/7/21)
+
 OPTION "logic" "ALL";
 BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)];
 x : SET OF BvPair;