mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

make check_relation::check_equiv() exit only when solver return SAT (ie, avoid false-positives with unknowns)

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-24 17:13:24 +01:00
parent 30eb461e01
commit f29d82858f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -429,7 +429,7 @@ namespace datalog {
if (res == l_false) {
IF_VERBOSE(3, verbose_stream() << objective << " verified\n";);
}
else {
else if (res == l_true) {
IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n";
verbose_stream() << mk_pp(fml1, m) << "\n";
verbose_stream() << mk_pp(fml2, m) << "\n";