| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2010-06-03 | Fixes 2 issues with assignments. The first is constructing an initial ↵ | Tim King | |
| assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions. | |||
 |
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