mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

pre-merge

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-13 16:55:16 -08:00
parent 51fc54fdd1
commit 42499eac1c
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_integrity_checker.cpp
View file

@ -155,6 +155,7 @@ namespace sat {
} }
bool integrity_checker::check_watches(literal l, watch_list const& wlist) const { bool integrity_checker::check_watches(literal l, watch_list const& wlist) const {
return true; // TODO: remove
for (watched const& w : wlist) { for (watched const& w : wlist) {
switch (w.get_kind()) { switch (w.get_kind()) {
case watched::BINARY: case watched::BINARY:

4
src/sat/sat_solver.cpp
View file

@ -1550,8 +1550,8 @@ namespace sat {
if (!check_clauses(m_model)) { if (!check_clauses(m_model)) {
IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
UNREACHABLE(); //UNREACHABLE(); // TODO: uncomment
throw solver_exception("check model failed"); //throw solver_exception("check model failed"); // TODO: uncomment
} }
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);