From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 17 Jun 2014 20:32:47 +0000 (-0400)
Subject: Fix for new CASC features, fixes Java builds.
X-Git-Tag: cvc5-1.0.0~6758^2~21
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fec81b07b6a9b8e5c573119c3fb8b87476e0b071;p=cvc5.git

Fix for new CASC features, fixes Java builds.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 247c367b4..28a45206f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3020,8 +3020,8 @@ void SmtEnginePrivate::processAssertions() {
     SortInference * si = d_smt.d_theoryEngine->getSortInference();
     si->simplify( d_assertionsToPreprocess );
     for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
-      d_smt.setPrintFuncInModel( it->first, false );
-      d_smt.setPrintFuncInModel( it->second, true );
+      d_smt.setPrintFuncInModel( it->first.toExpr(), false );
+      d_smt.setPrintFuncInModel( it->second.toExpr(), true );
     }
   }
 
@@ -4125,14 +4125,13 @@ void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) {
   d_theoryEngine->setUserAttribute(attr, expr.getNode());
 }
 
-void SmtEngine::setPrintFuncInModel( Node f, bool p ) {
+void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
   Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
-  Expr fe = f.toExpr();
   for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
     Command * c = d_modelGlobalCommands[i];
     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
     if(dfc != NULL) {
-      if( dfc->getFunction()==fe ){
+      if( dfc->getFunction()==f ){
         dfc->setPrintInModel( p );
       }
     }
@@ -4141,7 +4140,7 @@ void SmtEngine::setPrintFuncInModel( Node f, bool p ) {
     Command * c = (*d_modelCommands)[i];
     DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
     if(dfc != NULL) {
-      if( dfc->getFunction()==fe ){
+      if( dfc->getFunction()==f ){
         dfc->setPrintInModel( p );
       }
     }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c53156a3c..acf7954bc 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -656,7 +656,7 @@ public:
   /**
    * Set print function in model
    */
-  void setPrintFuncInModel( Node f, bool p );
+  void setPrintFuncInModel(Expr f, bool p);
   
 };/* class SmtEngine */