1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 92c866ffd..00a910567 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -65,8 +65,8 @@ public:
     d_has_simplified = false;
   }
   bool addEntry( FullModelChecker * m, Node c, Node v);
-  Node evaluate( FullModelChecker * m, std::vector<Node> inst );
-  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+  Node evaluate( FullModelChecker * m, std::vector<Node>& inst );
+  int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );
   void simplify( FullModelChecker * m );
   void debugPrint(const char * tr, Node op, FullModelChecker * m);
 };
@@ -141,6 +141,8 @@ public:
 
   /** process build model */
   void processBuildModel(TheoryModel* m, bool fullModel);
+  /** get current model value */
+  Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
 };
 
 }