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

reduce verbosity level of error message when equivalence checking fails

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-09 08:32:57 -07:00
parent d7da64f946
commit 44105b7aeb
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/rel/check_relation.cpp
View file

@ -430,12 +430,12 @@ namespace datalog {
IF_VERBOSE(3, verbose_stream() << objective << " verified\n";);
}
else if (res == l_true) {
IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
IF_VERBOSE(0, verbose_stream() << "NOT verified " << res << "\n";
verbose_stream() << mk_pp(fml1, m) << "\n";
verbose_stream() << mk_pp(fml2, m) << "\n";
verbose_stream().flush();
);
throw 0;
throw default_exception("operation was not verified");
}
}