From 4fd1f4a65c069245e6124b8da209e83ecd6b5295 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 11:34:55 -0700 Subject: [PATCH 1/2] 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; From fb624780d5f40ea5c9735f441c027c9001eeea48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 12:41:57 -0700 Subject: [PATCH 2/2] add checks in internalizer for issues of the form #227 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 54506882c..13999222f 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -617,8 +617,15 @@ namespace smt { mk_ite_cnstr(to_app(n)); add_ite_rel_watches(to_app(n)); break; + case OP_TRUE: + case OP_FALSE: + break; case OP_DISTINCT: case OP_IMPLIES: + case OP_XOR: + UNREACHABLE(); + case OP_OEQ: + case OP_INTERP: UNREACHABLE(); default: break;