More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

1 files changed, 4 insertions, 2 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 34cdd2e30..9f502c2ea 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1055,7 +1055,7 @@ GetInstantiationsCommand::GetInstantiationsCommand() throw() {
 
 void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    smtEngine->printInstantiations();
+    d_smtEngine = smtEngine;
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -1070,19 +1070,21 @@ void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    //d_result->toStream(out);
+    d_smtEngine->printInstantiations(out);
   }
 }
 
 Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   GetInstantiationsCommand* c = new GetInstantiationsCommand();
   //c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
   return c;
 }
 
 Command* GetInstantiationsCommand::clone() const {
   GetInstantiationsCommand* c = new GetInstantiationsCommand();
   //c->d_result = d_result;
+  c->d_smtEngine = d_smtEngine;
   return c;
 }