From ad2e6ff2b42ef1d0e8e1ea4dde1c1b752666b98b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Mar 2020 12:49:48 -0700 Subject: [PATCH] fix #3607 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 671e46440..9536c7f40 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -657,7 +657,7 @@ namespace smt { case OP_DISTINCT: case OP_IMPLIES: case OP_XOR: - UNREACHABLE(); + throw default_exception("formula has not been simplified"); case OP_OEQ: UNREACHABLE(); default: