bug fixes to model gen

2 files changed, 2 insertions, 3 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3a4fd90e9..5de1cd0b1 100644
--- 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 a1eec9d4c..fe1f3106e 100644
--- 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);