Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.

2 files changed, 28 insertions, 2 deletions

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index fb80b27f7..de1a60da4 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -48,6 +48,31 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
       return NodeManager::currentNM()->mkConst(tf);
     }
   }
+  if(n.getType().isBoolean()) {
+    bool tf = n.getConst<bool>();
+    if(asType.isBitVector(1u)) {
+      return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
+    }
+    if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
+      const Datatype& asDatatype = asType.getConst<Datatype>();
+      return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
+    }
+  }
+  if(n.getType().isRecord() && asType.isRecord()) {
+    Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
+    const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
+    const Record& asRec = asType.getConst<Record>();
+    Assert(rec.getNumFields() == asRec.getNumFields());
+    Assert(n.getNumChildren() == asRec.getNumFields());
+    NodeBuilder<> b(n.getKind());
+    b << asType;
+    for(size_t i = 0; i < n.getNumChildren(); ++i) {
+      b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
+    }
+    Node out = b;
+    Debug("boolean-terms") << "+++ returning record " << out << endl;
+    return out;
+  }
   Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
   if(n.getType().isArray()) {
     Assert(asType.isArray());
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 2c5844cd4..b4ac8d27e 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -51,7 +51,9 @@ Node TheoryModel::getValue( TNode n ) const{
   //apply substitutions
   Node nn = d_substitutions.apply( n );
   //get value in model
-  return getModelValue( nn );
+  nn = getModelValue( nn );
+  Assert(nn.isConst() || nn.getKind() == kind::LAMBDA);
+  return nn;
 }
 
 Expr TheoryModel::getValue( Expr expr ) const{
@@ -150,7 +152,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       if(val.getKind() == kind::CARDINALITY_CONSTRAINT) {
         val = NodeManager::currentNM()->mkConst(getCardinality(val[0].getType().toType()).getFiniteCardinality() <= val[1].getConst<Rational>().getNumerator());
       }
-      Assert(hasBoundVars || val.isConst());
       return val;
     }