mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

#5429

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-31 11:00:12 -07:00
parent e5401a4303
commit 6a9241ff0f
5 changed files with 44 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/shell/drat_frontend.cpp
View file

@ -122,12 +122,17 @@ class smt_checker {
m_input_solver->assert_expr(lit2expr(~lit));
lbool is_sat = m_input_solver->check_sat();
if (is_sat != l_false) {
std::cout << "did not verify: " << lits << "\n";
for (sat::literal lit : lits) {
std::cout << lit2expr(lit) << "\n";
}
std::cout << "did not verify: " << is_sat << " " << lits << "\n";
for (sat::literal lit : lits)
std::cout << lit2expr(lit) << "\n";
std::cout << "\n";
m_input_solver->display(std::cout);
if (is_sat == l_true) {
model_ref mdl;
m_input_solver->get_model(mdl);
std::cout << *mdl << "\n";
}
exit(0);
}
m_input_solver->pop(1);