diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-07-29 14:22:10 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-29 17:22:10 +0000 |
| commit | 63dfa2730bac42fed9dda6aa5fb3d57e6cadfcc0 (patch) | |
| tree | 76cc41180fa96a857aaa6aebe9bf33f8922d6b95 /test/regress/regress0 | |
| parent | 040c3a7a345f6e76f410793da4c376d225b62162 (diff) | |
[proofs] Set BV solver to better proof-producing one when proofs on (#6903)
Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/fp/issue-5524.smt2 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2 index 741d77a19..3902f9c37 100644 --- a/test/regress/regress0/fp/issue-5524.smt2 +++ b/test/regress/regress0/fp/issue-5524.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --bv-solver=bitblast ; EXPECT: unsat (set-logic QF_FP) (declare-fun fpv5 () Float32) |