From 44105b7aeb8ec6e85dfba23321eaa6838695d1f3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Sep 2015 08:32:57 -0700 Subject: [PATCH] reduce verbosity level of error message when equivalence checking fails Signed-off-by: Nikolaj Bjorner --- src/muz/rel/check_relation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 534a66284..7c6dac5e4 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -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"); } }