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: