Fix smt2 printing of fun-def. Simplification of mbqi interface.

1 files changed, 8 insertions, 2 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a98a106a1..7648a1587 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -32,6 +32,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 
@@ -589,9 +590,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::INST_PATTERN:
     break;
   case kind::INST_PATTERN_LIST:
-    // TODO user patterns
     for(unsigned i=0; i<n.getNumChildren(); i++) {
-      out << ":pattern " << n[i];
+      if( n[i].getKind()==kind::INST_ATTRIBUTE ){
+        if( n[i][0].getAttribute(theory::FunDefAttribute()) ){
+          out << ":fun-def";
+        }
+      }else{
+        out << ":pattern " << n[i];
+      }
     }
     return;
     break;