From f29d82858f937ef2965eaffc552b9df0e0367c3b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 24 Jun 2015 17:13:24 +0100 Subject: [PATCH] make check_relation::check_equiv() exit only when solver return SAT (ie, avoid false-positives with unknowns) Signed-off-by: Nuno Lopes --- src/muz/rel/check_relation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 0ba03200b..534a66284 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -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";