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 /test | |
| parent | a4e5c52452519067da198dc31991dc4c92877fcb (diff) | |
Disable ordering heuristic for justification by default (#6848)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress1/rels/bv1p.cvc | 4 |
1 files changed, 4 insertions, 0 deletions
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; |