mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

print validation failures

Browse source
This commit is contained in:
Jakob Rath 2024-03-13 14:12:10 +01:00
parent 7da7e99ca2
commit 5d1602b6c7
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/smt/intblast_solver.cpp
View file

@ -308,6 +308,7 @@ namespace intblast {
IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n");
if (r == l_true) { if (r == l_true) {
verbose_stream() << "validation failed: " << name << "\n";
IF_VERBOSE(0, IF_VERBOSE(0,
model_ref mdl; model_ref mdl;
m_solver->get_model(mdl); m_solver->get_model(mdl);