From 51dc426b0e217a4f1292be995f5473a7f2d27ad8 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 17 Jun 2014 16:32:47 -0400
Subject: [PATCH] Fix for new CASC features, fixes Java builds.

---
 src/smt/smt_engine.cpp | 11 +++++------
 src/smt/smt_engine.h   |  2 +-
 2 files changed, 6 insertions(+), 7 deletions(-)

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 */
 
-- 
2.30.2