projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bdaa304) | patch
* Add assertion in TheoryModel code to ensure we don't get inconsistent
authorMorgan Deters <mdeters@gmail.com>
Tue, 9 Oct 2012 13:22:28 +0000 (13:22 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 9 Oct 2012 13:22:28 +0000 (13:22 +0000)
commit5b65d0f80d56731fd7d07f491973bad14a85566e
tree4aafa4742804ff87408a1da7523d799851a028c0tree
parentbdaa3049467fd17d3fb95701f7946a4bf0f5206acommit | diff
* Add assertion in TheoryModel code to ensure we don't get inconsistent
  substitutions for solved variables.  Related to bug 418 (and might
  resolve it).

* Respect phase-locking in Minisat (one phase-saving site was unguarded).

(this commit was certified error- and warning-free by the test-and-commit script.)
src/prop/minisat/core/Solver.cc diff | blob | history
src/theory/model.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history