Clean out opensmt #3158
Clean out opensmt #3158
Conversation
kroening
commented
Oct 14, 2018
•
kroening
commented
- Each commit message has a non-empty body, explaining why the change was made.
- My contribution is formatted in line with CODING_STANDARD.md.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
kroening
requested review from
martin-cs,
peterschrammel,
smowton and
tautschnig
as code owners
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 014eea4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87877503
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 54cfd56).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87881419
|
The idea is that one day you can run all the tests in regression/cbmc with --cprover-smt2! We don't really need separate tests. |
There was a problem hiding this comment.
Can we please not do "to_integer now converts uninterpreted bitvectors"? That completely contradicts what the comments say what a bv_typet is. I believe any interpretation of a bv_typet as a signed or unsigned bitvector should go via a type cast, bit- or byte extract operation. Or we just kill bv_typet completely and use unsignedbv_typet instead.
src/cbmc/cbmc_parse_options.h
Outdated
| @@ -46,7 +46,8 @@ class optionst; | |||
| OPT_GOTO_CHECK \ | |||
| "(no-assertions)(no-assumptions)" \ | |||
| "(xml-ui)(xml-interface)(json-ui)" \ | |||
| "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \ | |||
| "(smt1)(smt2)(fpa)" \ | |||
| "(cprover-smt2)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \ | |||
There was a problem hiding this comment.
OpenSMT is still being developed by Hana and Natasha's teams; do we really want to remove support?
There was a problem hiding this comment.
Yes; it does not support any theories that we use.
|
@smowton : systematic testing of the SMT solvers would be good but I think it might have to be as part of a larger campaign of "let's make SMT solvers the first choice for back-ends" and each time we've done the benchmarking on this ... it hasn't (yet) justified the effort. |
Support was dropped in April 2018.
kroening
force-pushed
the
cprover-smt2
branch
from
54cfd56 to
145c895
Compare
|
@tautschnig : This PR no longer includes the changes you objected to. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 145c895).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90441669
