From 4fd1f4a65c069245e6124b8da209e83ecd6b5295 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 11:34:55 -0700 Subject: [PATCH] add handler for abuse of OP_IMPLIES Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 4f810727a..54506882c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -618,6 +618,7 @@ namespace smt { add_ite_rel_watches(to_app(n)); break; case OP_DISTINCT: + case OP_IMPLIES: UNREACHABLE(); default: break;