mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

fix debug build

Browse source
This commit is contained in:
Nuno Lopes 2022-06-17 14:35:33 +01:00
parent 73a24ca0a9
commit d9fcfdab34
8 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -1756,14 +1756,14 @@ namespace smtfd {
expr_ref val0 = (*m_model)(a);
expr_ref val1 = (*m_model)(abs(a));
if (is_ground(a) && val0 != val1 && val0->get_sort() == val1->get_sort()) {
std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
//std::cout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
found_bad = true;
}
}
if (found_bad) {
std::cout << "core: " << core << "\n";
std::cout << *m_model.get() << "\n";
exit(0);
//std::cout << "core: " << core << "\n";
//std::cout << *m_model.get() << "\n";
UNREACHABLE();
});
if (!has_q) {