Fallbackeval

2 files changed, 11 insertions, 4 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index b50b811bf..1d5b56bd4 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -199,8 +199,11 @@ Node Evaluator::eval(TNode n,
         }
 
         default:
-          std::cout << "Not supported: " << currNodeVal << std::endl;
-          std::exit(1);
+        {
+          Debug("evaluator") << "Kind " << currNodeVal.getKind()
+                             << " not supported" << std::endl;
+          d_results[currNode] = Result();
+        }
       }
     }
   }
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 35ba2b3d9..17aeb4381 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -93,9 +93,13 @@ struct Result
     switch (d_tag)
     {
       case Result::BITVECTOR: return nm->mkConst(d_bv);
+      case Result::BOOL: return nm->mkConst(d_bool);
       default:
-        std::cout << "Not supported:( " << d_tag << std::endl;
-        std::exit(1);
+      {
+        Debug("evaluator") << "Missing conversion from " << d_tag << " to node"
+                           << std::endl;
+        return Node();
+      }
     }
 
     return Node();