fix for --produce-models with CVC4 presentation language

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 01ce73be1d64954f5f2f4e69e600fd6d8583b35c..a182d89275ceca2092e06d104db8350d2344745a 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1889,6 +1889,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
 void SmtEngine::addToModelType( Type& t ){
   Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
   SmtScope smts(this);
+  finalOptionsAreSet();
   if( Options::current()->produceModels ) {
     d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
   }
@@ -1897,6 +1898,7 @@ void SmtEngine::addToModelType( Type& t ){
 void SmtEngine::addToModelFunction( Expr& e ){
   Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
   SmtScope smts(this);
+  finalOptionsAreSet();
   if( Options::current()->produceModels ) {
     d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
   }