From fb624780d5f40ea5c9735f441c027c9001eeea48 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 31 Oct 2015 12:41:57 -0700
Subject: [PATCH] add checks in internalizer for issues of the form #227

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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;