More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index cbabc9542..c61a61940 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -9,9 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief 
+ ** \brief
+ **
  **
- ** 
  **/
 
 #include "smt/model_postprocessor.h"
@@ -92,6 +92,9 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     return n;
   }
   NodeBuilder<> b(n.getKind());
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    b << n.getOperator();
+  }
   TypeNode::iterator t = asType.begin();
   for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
     Assert(t != asType.end());