| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-20 | Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are ↵ | yoni206 | |
| enabled (#1801) Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable). This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user. | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback