mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

#5261

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-10 13:33:37 -07:00
parent f02fbb49bb
commit 897a2d6470
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/shell/dimacs_frontend.cpp
View file

@ -264,15 +264,15 @@ unsigned read_dimacs(char const * file_name) {
} }
switch (r) { switch (r) {
case l_true: case l_true:
std::cout << "sat\n"; std::cout << "s SATISFIABLE\n";
if (file_name && gparams::get_ref().get_bool("model_validate", false)) verify_solution(file_name); if (file_name && gparams::get_ref().get_bool("model_validate", false)) verify_solution(file_name);
display_model(*g_solver); display_model(*g_solver);
break; break;
case l_undef: case l_undef:
std::cout << "unknown\n"; std::cout << "s UNKNOWN\n";
break; break;
case l_false: case l_false:
std::cout << "unsat\n"; std::cout << "s UNSATISFIABLE\n";
if (p.get_bool("dimacs.core", false)) { if (p.get_bool("dimacs.core", false)) {
display_core(*g_solver, tracking_clauses); display_core(*g_solver, tracking_clauses);
} }