From fb2f314ac9a187538bfa2c09f2d8bdc3465804a9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 8 Jul 2021 16:16:25 -0500 Subject: [PATCH] Disable ordering heuristic for justification by default (#6848) --- src/options/decision_options.toml | 2 +- test/regress/regress1/rels/bv1p.cvc | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) 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; -- 2.30.2