diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-08 16:16:25 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-08 21:16:25 +0000 |
| commit | fb2f314ac9a187538bfa2c09f2d8bdc3465804a9 (patch) | |
| tree | 61cab6663b84158a28e22add1de88f1b5e54afff | |
| parent | a4e5c52452519067da198dc31991dc4c92877fcb (diff) | |
Disable ordering heuristic for justification by default (#6848)
| -rw-r--r-- | src/options/decision_options.toml | 2 | ||||
| -rw-r--r-- | test/regress/regress1/rels/bv1p.cvc | 4 |
2 files changed, 5 insertions, 1 deletions
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; |