From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 8 Jul 2021 21:16:25 +0000 (-0500)
Subject: Disable ordering heuristic for justification by default (#6848)
X-Git-Tag: cvc5-1.0.0~1513
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb2f314ac9a187538bfa2c09f2d8bdc3465804a9;p=cvc5.git

Disable ordering heuristic for justification by default (#6848)
---

diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 840eaa08f..8cc2bf2fe 100644
--- 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 0e8803ce6..ed9fdce1f 100644
--- 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;