From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 9 Oct 2010 06:13:17 +0000 (+0000)
Subject: bug fixes to model gen
X-Git-Tag: cvc5-1.0.0~8816
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e40b31aa45ca9e34b92875a8a1079ae953922956;p=cvc5.git

bug fixes to model gen
---

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);