bug fixes to model gen

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a4fd90e998502b837a598637dc864571d1cd24c..5de1cd0b19490d4b9b1b163edfe293f15997e2b8 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -410,7 +410,7 @@ Expr SmtEngine::getValue(Expr e)
   Node resultNode = d_theoryEngine->getValue(n);
 
   // type-check the result we got
-  Assert(resultNode.getType(true) == eNode.getType());
+  Assert(resultNode.isNull() || resultNode.getType(true) == eNode.getType());
   return Expr(d_exprManager, new Node(resultNode));
 }
 

diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index a1eec9d4c37564b0bc62096a58e4a7439814ea24..fe1f3106e71c0a38a6d5a03f91fcd29c4af21c8e 100644 (file)
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -462,10 +462,9 @@ Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) {
     if(n.getType().isBoolean()) {
       if(d_cc.areCongruent(d_trueNode, n)) {
         return nodeManager->mkConst(true);
-      } else if(d_cc.areCongruent(d_trueNode, n)) {
+      } else if(d_cc.areCongruent(d_falseNode, n)) {
         return nodeManager->mkConst(false);
       }
-      return Node::null();
     }
     return d_cc.normalize(n);