From 24e4f19d76c17574bb6c9d1d64b22f6dd316978e Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Jan 2017 14:08:21 +0000
Subject: [PATCH 1/7] build fix

---
 scripts/mk_win_dist.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index 9d3abaf2c..0e7fab490 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -315,7 +315,7 @@ def main():
         init_project_def()
         mk_dist_dirs()
         cp_licenses()
-        cp_vs_runtime()
+        cp_vs_runtimes()
         mk_zip()
 
 main()

From 00a50eea7f439fad4ba8bb981eedf15e076bfb41 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Jan 2017 15:05:58 +0000
Subject: [PATCH 2/7] Added (include ...) SMT2 command.

---
 src/shell/smtlib_frontend.cpp |  2 ++
 src/smt/smt2_extra_cmds.cpp   | 47 +++++++++++++++++++++++++++++++++++
 src/smt/smt2_extra_cmds.h     | 26 +++++++++++++++++++
 3 files changed, 75 insertions(+)
 create mode 100644 src/smt/smt2_extra_cmds.cpp
 create mode 100644 src/smt/smt2_extra_cmds.h

diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 31c964ae0..c9fa69221 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -29,6 +29,7 @@ Revision History:
 #include"opt_cmds.h"
 #include"polynomial_cmds.h"
 #include"subpaving_cmds.h"
+#include"smt2_extra_cmds.h"
 #include"smt_strategic_solver.h"
 #include"smt_solver.h"
 
@@ -113,6 +114,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
     install_polynomial_cmds(ctx);
     install_subpaving_cmds(ctx);
     install_opt_cmds(ctx);
+    install_smt2_extra_cmds(ctx);
 
     g_cmd_context = &ctx;
     signal(SIGINT, on_ctrl_c);
diff --git a/src/smt/smt2_extra_cmds.cpp b/src/smt/smt2_extra_cmds.cpp
new file mode 100644
index 000000000..866a1178e
--- /dev/null
+++ b/src/smt/smt2_extra_cmds.cpp
@@ -0,0 +1,47 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    smt2_extra_cmds.cpp
+
+Abstract:
+
+    Additional SMT-specific commands.
+
+Author:
+
+    Christoph (cwinter) 2017-01-16
+
+Notes:
+
+--*/
+#include"cmd_context.h"
+#include"smt2parser.h"
+#include"smt2_extra_cmds.h"
+
+class include_cmd : public cmd {
+    char const * m_filename;
+public:
+    include_cmd() : cmd("include"), m_filename(0) {}
+    virtual char const * get_usage() const { return "<string>"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "include a file"; }
+    virtual unsigned get_arity() const { return 1; }
+    virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_STRING; }
+    virtual void set_next_arg(cmd_context & ctx, char const * val) { m_filename = val; }
+    virtual void failure_cleanup(cmd_context & ctx) {}
+    virtual void execute(cmd_context & ctx) {
+        std::ifstream is(m_filename);
+        if (is.bad() || is.fail())
+            throw cmd_exception(std::string("failed to open file '") + m_filename + "'");
+        parse_smt2_commands(ctx, is, false);
+        is.close();
+    }
+    virtual void prepare(cmd_context & ctx) { reset(ctx); }
+    virtual void reset(cmd_context & ctx) { m_filename = 0; }
+    virtual void finalize(cmd_context & ctx) { reset(ctx); }
+};
+
+void install_smt2_extra_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(include_cmd));
+}
\ No newline at end of file
diff --git a/src/smt/smt2_extra_cmds.h b/src/smt/smt2_extra_cmds.h
new file mode 100644
index 000000000..947f5ed7a
--- /dev/null
+++ b/src/smt/smt2_extra_cmds.h
@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    smt2_extra_cmds.h
+
+Abstract:
+
+    Additional SMT-specific commands.
+
+Author:
+
+    Christoph (cwinter) 2017-01-16
+
+Notes:
+
+--*/
+#ifndef SMT2_EXTRA_CMDS_H_
+#define SMT2_EXTRA_CMDS_H_
+
+class cmd_context;
+
+void install_smt2_extra_cmds(cmd_context & ctx);
+
+#endif /* SMT2_EXTRA_CMDS_H_ */

From 090a331d79648b7eb76a49ac1fd22c80a63a19a8 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 9 Jan 2017 14:51:01 +0000
Subject: [PATCH 3/7] Added filenames to error messages for when we have more
 than one file.

---
 src/parsers/smt2/smt2parser.cpp | 195 ++++++++++++++++----------------
 src/parsers/smt2/smt2parser.h   |   2 +-
 2 files changed, 101 insertions(+), 96 deletions(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index bb0c5bfb9..d2b55af1d 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -109,7 +109,6 @@ namespace smt2 {
         typedef std::pair<symbol, expr*> named_expr;
         named_expr           m_last_named_expr;
 
-
         ast_manager & m() const { return m_ctx.m(); }
         pdecl_manager & pm() const { return m_ctx.pm(); }
         sexpr_manager & sm() const { return m_ctx.sm(); }
@@ -117,7 +116,7 @@ namespace smt2 {
         bool m_ignore_user_patterns;
         bool m_ignore_bad_patterns;
         bool m_display_error_for_vs;
-        
+
         bool ignore_user_patterns() const { return m_ignore_user_patterns; }
         bool ignore_bad_patterns() const  { return m_ignore_bad_patterns; }
         bool use_vs_format() const        { return m_display_error_for_vs; }
@@ -129,7 +128,7 @@ namespace smt2 {
                 m_decl(d), m_spos(spos) {
             }
         };
-        
+
         typedef psort_frame sort_frame;
 
         enum expr_frame_kind { EF_APP, EF_LET, EF_LET_DECL, EF_QUANT, EF_ATTR_EXPR, EF_PATTERN };
@@ -138,17 +137,17 @@ namespace smt2 {
             expr_frame_kind m_kind;
             expr_frame(expr_frame_kind k):m_kind(k) {}
         };
-        
+
         struct app_frame : public expr_frame {
             symbol   m_f;
             unsigned m_expr_spos;
             unsigned m_param_spos;
             bool     m_as_sort;
             app_frame(symbol const & f, unsigned expr_spos, unsigned param_spos, bool as_sort):
-                expr_frame(EF_APP), 
-                m_f(f), 
-                m_expr_spos(expr_spos), 
-                m_param_spos(param_spos), 
+                expr_frame(EF_APP),
+                m_f(f),
+                m_expr_spos(expr_spos),
+                m_param_spos(param_spos),
                 m_as_sort(as_sort) {}
         };
 
@@ -163,8 +162,8 @@ namespace smt2 {
             unsigned m_sort_spos;
             unsigned m_expr_spos;
             quant_frame(bool forall, unsigned pat_spos, unsigned nopat_spos, unsigned sym_spos, unsigned sort_spos, unsigned expr_spos):
-                expr_frame(EF_QUANT), m_forall(forall), m_weight(1), 
-                m_pat_spos(pat_spos), m_nopat_spos(nopat_spos), 
+                expr_frame(EF_QUANT), m_forall(forall), m_weight(1),
+                m_pat_spos(pat_spos), m_nopat_spos(nopat_spos),
                 m_sym_spos(sym_spos), m_sort_spos(sort_spos),
                 m_expr_spos(expr_spos) {}
         };
@@ -175,7 +174,7 @@ namespace smt2 {
             unsigned m_expr_spos;
             let_frame(unsigned sym_spos, unsigned expr_spos):expr_frame(EF_LET), m_in_decls(true), m_sym_spos(sym_spos), m_expr_spos(expr_spos) {}
         };
-        
+
         struct let_decl_frame : public expr_frame {
             let_decl_frame():expr_frame(EF_LET_DECL) {}
         };
@@ -186,9 +185,9 @@ namespace smt2 {
             unsigned     m_expr_spos;
             symbol       m_last_symbol;
             attr_expr_frame(expr_frame * prev, unsigned sym_spos, unsigned expr_spos):
-                expr_frame(EF_ATTR_EXPR), 
-                m_prev(prev), 
-                m_sym_spos(sym_spos), 
+                expr_frame(EF_ATTR_EXPR),
+                m_prev(prev),
+                m_sym_spos(sym_spos),
                 m_expr_spos(expr_spos) {}
         };
 
@@ -228,12 +227,12 @@ namespace smt2 {
                 m_expr_stack = alloc(expr_ref_vector, m());
             return *(m_expr_stack.get());
         }
-        
+
         template<typename T>
         static unsigned size(scoped_ptr<T> & v) {
             return v.get() == 0 ? 0 : v->size();
         }
-        
+
         template<typename T>
         static void shrink(scoped_ptr<T> & v, unsigned old_sz) {
             if (v.get() == 0) {
@@ -255,7 +254,7 @@ namespace smt2 {
                 m_nopattern_stack = alloc(expr_ref_vector, m());
             return *(m_nopattern_stack.get());
         }
-       
+
         svector<symbol> & symbol_stack() {
             return m_symbol_stack;
         }
@@ -328,7 +327,7 @@ namespace smt2 {
         bool sync_after_error() {
             while (true) {
                 try {
-                    while (curr_is_rparen()) 
+                    while (curr_is_rparen())
                         next();
                     if (m_num_open_paren < 0)
                         m_num_open_paren = 0;
@@ -337,7 +336,7 @@ namespace smt2 {
                     SASSERT(m_num_open_paren >= 0);
                     while (m_num_open_paren > 0 || !curr_is_lparen()) {
                         TRACE("sync", tout << "sync(): curr: " << curr() << "\n";
-                              tout << "m_num_open_paren: " << m_num_open_paren << ", line: " << m_scanner.get_line() << ", pos: " 
+                              tout << "m_num_open_paren: " << m_num_open_paren << ", line: " << m_scanner.get_line() << ", pos: "
                               << m_scanner.get_pos() << "\n";);
                         if (curr() == scanner::EOF_TOKEN) {
                             return false;
@@ -365,7 +364,7 @@ namespace smt2 {
             }
             throw parser_exception(msg);
         }
-        
+
         symbol const & curr_id() const { return m_scanner.get_id(); }
         rational curr_numeral() const { return m_scanner.get_number(); }
 
@@ -402,15 +401,20 @@ namespace smt2 {
         void check_int_or_float(char const * msg) { if (!curr_is_int() && !curr_is_float()) throw parser_exception(msg); }
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
+        char const * m_current_file;
+        void set_current_file(char const * s) { m_current_file = s; }
+
         void error(unsigned line, unsigned pos, char const * msg) {
             m_ctx.set_cancel(false);
             if (use_vs_format()) {
                 m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
                 if (msg[strlen(msg)-1] != '\n')
-                    m_ctx.diagnostic_stream() << std::endl; 
+                    m_ctx.diagnostic_stream() << std::endl;
             }
             else {
-                m_ctx.regular_stream() << "(error \"line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
+                m_ctx.regular_stream() << "(error \"";
+                if (m_current_file) m_ctx.regular_stream() << m_current_file << ": ";
+                m_ctx.regular_stream()<< "line " << line << " column " << pos << ": " << escaped(msg, true) << "\")" << std::endl;
             }
             if (m_ctx.exit_on_error()) {
                 exit(1);
@@ -431,7 +435,7 @@ namespace smt2 {
                 m_ctx.regular_stream() << "(error : " << escaped(msg, true) << "\")" << std::endl;
             }
         }
-        
+
         void unknown_sort(symbol id, char const* context = "") {
             std::string msg = context;
             if (context[0]) msg += ": ";
@@ -444,10 +448,10 @@ namespace smt2 {
             unsigned num_parens = 0;
             do {
                 switch (curr()) {
-                case scanner::LEFT_PAREN: 
-                    num_parens++; 
+                case scanner::LEFT_PAREN:
+                    num_parens++;
                     break;
-                case scanner::RIGHT_PAREN: 
+                case scanner::RIGHT_PAREN:
                     if (num_parens == 0)
                         throw parser_exception("invalid s-expression, unexpected ')'");
                     num_parens--;
@@ -565,7 +569,7 @@ namespace smt2 {
                 else {
                     if (ignore_unknow_sort)
                         return 0;
-                    unknown_sort(id); 
+                    unknown_sort(id);
                     UNREACHABLE();
                     return 0;
                 }
@@ -579,7 +583,7 @@ namespace smt2 {
             check_identifier("invalid indexed sort, symbol expected");
             symbol id = curr_id();
             psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == 0) 
+            if (d == 0)
                 unknown_sort(id);
             next();
             sbuffer<unsigned> args;
@@ -604,13 +608,13 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
             psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == 0) 
+            if (d == 0)
                 unknown_sort(id);
             next();
             void * mem      = m_stack.allocate(sizeof(psort_frame));
             new (mem) psort_frame(*this, d, psort_stack().size());
         }
-        
+
         void pop_psort_app_frame() {
             SASSERT(curr_is_rparen());
             psort_frame * fr = static_cast<psort_frame*>(m_stack.top());
@@ -647,7 +651,7 @@ namespace smt2 {
                 else {
                     check_lparen_next("invalid sort, symbol, '_' or '(' expected");
                     if (!curr_is_identifier())
-                        throw parser_exception("invalid sort, symbol or '_' expected"); 
+                        throw parser_exception("invalid sort, symbol or '_' expected");
                     if (curr_id_is_underscore()) {
                         psort_stack().push_back(pm().mk_psort_cnst(parse_indexed_sort()));
                     }
@@ -665,13 +669,13 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             symbol id = curr_id();
             psort_decl * d = m_ctx.find_psort_decl(id);
-            if (d == 0) 
+            if (d == 0)
                 unknown_sort(id);
             next();
             void * mem      = m_stack.allocate(sizeof(sort_frame));
             new (mem) sort_frame(*this, d, sort_stack().size());
         }
-        
+
         void pop_sort_app_frame() {
             SASSERT(curr_is_rparen());
             sort_frame * fr = static_cast<sort_frame*>(m_stack.top());
@@ -710,8 +714,8 @@ namespace smt2 {
                 }
                 else {
                     check_lparen_next("invalid sort, symbol, '_' or '(' expected");
-                    if (!curr_is_identifier()) 
-                        throw parser_exception(std::string(context) + " invalid sort, symbol or '_' expected"); 
+                    if (!curr_is_identifier())
+                        throw parser_exception(std::string(context) + " invalid sort, symbol or '_' expected");
                     if (curr_id_is_underscore()) {
                         sort_stack().push_back(parse_indexed_sort());
                     }
@@ -726,7 +730,7 @@ namespace smt2 {
         }
 
         unsigned parse_sorts(char const* context) {
-            unsigned sz = 0;            
+            unsigned sz = 0;
             check_lparen_next(context);
             while (!curr_is_rparen()) {
                 parse_sort(context);
@@ -949,7 +953,7 @@ namespace smt2 {
         }
 
         // parse expression state
-        enum pe_state { 
+        enum pe_state {
             PES_EXPR,  // expecting <expr>
             PES_DECL,  // expecting (<id> <expr>)
             PES_PATTERN,
@@ -1015,7 +1019,7 @@ namespace smt2 {
                     else {
                         // just consume pattern
                         next();
-                        consume_sexpr(); 
+                        consume_sexpr();
                     }
                 }
                 else if (id == m_nopattern) {
@@ -1036,7 +1040,7 @@ namespace smt2 {
                     str << "unknown attribute " << id;
                     warning_msg("%s", str.str().c_str());
                     next();
-                    // just consume the 
+                    // just consume the
                     consume_sexpr();
                 }
                 if (curr_is_rparen())
@@ -1051,13 +1055,13 @@ namespace smt2 {
             switch (fr->m_kind) {
             case EF_LET:
                 return static_cast<let_frame*>(fr)->m_in_decls ? PES_DECL : PES_EXPR;
-            case EF_ATTR_EXPR: 
+            case EF_ATTR_EXPR:
                 return consume_attributes(static_cast<attr_expr_frame*>(fr));
             default:
                 return PES_EXPR;
             }
         }
-        
+
         void parse_numeral(bool is_int) {
             SASSERT(!is_int || curr_is_int());
             SASSERT(is_int || curr_is_float());
@@ -1095,7 +1099,7 @@ namespace smt2 {
                 expr_stack().push_back(0); // empty pattern
                 return;
             }
-            
+
             if (curr_is_lparen()) {
                 // multi-pattern
                 void * mem      = m_stack.allocate(sizeof(pattern_frame));
@@ -1185,9 +1189,9 @@ namespace smt2 {
             SASSERT(curr_id_is_forall() || curr_id_is_exists());
             SASSERT(!is_forall || curr_id_is_forall());
             SASSERT(is_forall || curr_id_is_exists());
-            next(); 
+            next();
             void * mem      = m_stack.allocate(sizeof(quant_frame));
-            new (mem) quant_frame(is_forall, pattern_stack().size(), nopattern_stack().size(), symbol_stack().size(), 
+            new (mem) quant_frame(is_forall, pattern_stack().size(), nopattern_stack().size(), symbol_stack().size(),
                                   sort_stack().size(), expr_stack().size());
             m_num_expr_frames++;
             unsigned num_vars = parse_sorted_vars();
@@ -1229,11 +1233,11 @@ namespace smt2 {
                 next();
                 return r;
             }
-            check_lparen_next("invalid (indexed) identifier, '(_' or symbol expected"); 
+            check_lparen_next("invalid (indexed) identifier, '(_' or symbol expected");
             return parse_indexed_identifier_core();
         }
 
-        // parse: 
+        // parse:
         //    'as' <identifier> <sort> ')'
         //    '_'  <identifier> <num>+ ')'
         //    'as' <identifier '(' '_' <identifier> (<num>|<func-decl-ref>)+ ')' <sort> ')'
@@ -1255,7 +1259,7 @@ namespace smt2 {
             }
         }
 
-        // parse: 
+        // parse:
         //    <identifier>
         //    '(' 'as' <identifier> <sort> ')'
         //    '(' '_'  <identifier> <num>+ ')'
@@ -1281,8 +1285,8 @@ namespace smt2 {
             throw parser_exception(msg.c_str());
         }
 
-        rational m_last_bv_numeral; // for bv, bvbin, bvhex 
-        
+        rational m_last_bv_numeral; // for bv, bvbin, bvhex
+
         // return true if *s == [0-9]+
         bool is_bv_decimal(char const * s) {
             TRACE("is_bv_num", tout << "is_bv_decimal: " << s << "\n";);
@@ -1321,7 +1325,7 @@ namespace smt2 {
                 return false;
             return true;
         }
-        
+
         // return true if *s == hex[0-9,a-f,A-F]+
         bool is_bv_hex(char const * s) {
             SASSERT(*s == 'h');
@@ -1329,7 +1333,7 @@ namespace smt2 {
             if (*s != 'e') return false;
             ++s;
             if (*s != 'x') return false;
-            ++s; 
+            ++s;
             rational & n = m_last_bv_numeral;
             unsigned i = 0;
             n = rational(0);
@@ -1340,7 +1344,7 @@ namespace smt2 {
                 }
                 else if ('a' <= *s && *s <= 'f') {
                     n *= rational(16);
-                    n += rational(10 + (*s - 'a')); 
+                    n += rational(10 + (*s - 'a'));
                 }
                 else if ('A' <= *s && *s <= 'F') {
                     n *= rational(16);
@@ -1357,11 +1361,11 @@ namespace smt2 {
             }
         }
 
-        // Return true if 
+        // Return true if
         //    n == bv[0-9]+  OR
         //    n == bvhex[0-9,a-f,A-F]+ OR
-        //    n == bvbin[0-1]+ 
-        // It store the bit-vector value in m_last_bv_numeral   
+        //    n == bvbin[0-1]+
+        // It store the bit-vector value in m_last_bv_numeral
         bool is_bv_num(symbol const & n) {
             char const * s = n.bare_str();
             if (*s != 'b') return false;
@@ -1405,7 +1409,7 @@ namespace smt2 {
             }
             next();
         }
-        
+
         // if has_as == true, then the sort of t must be equal to sort_stack().pop_back()
         // if that is the case, pop the top of sort_stack()
         void check_qualifier(expr * t, bool has_as) {
@@ -1543,7 +1547,7 @@ namespace smt2 {
             unsigned num_args    = expr_stack().size() - fr->m_expr_spos;
             unsigned num_indices = m_param_stack.size() - fr->m_param_spos;
             expr_ref t_ref(m());
-            m_ctx.mk_app(fr->m_f, 
+            m_ctx.mk_app(fr->m_f,
                          num_args,
                          expr_stack().c_ptr() + fr->m_expr_spos,
                          num_indices,
@@ -1627,7 +1631,7 @@ namespace smt2 {
                 fr->m_qid = symbol(m_scanner.get_line());
             if (!m().is_bool(expr_stack().back()))
                 throw parser_exception("quantifier body must be a Boolean expression");
-            quantifier * new_q = m().mk_quantifier(fr->m_forall, 
+            quantifier * new_q = m().mk_quantifier(fr->m_forall,
                                                    num_decls,
                                                    sort_stack().c_ptr() + fr->m_sort_spos,
                                                    symbol_stack().c_ptr() + fr->m_sym_spos,
@@ -1688,7 +1692,7 @@ namespace smt2 {
             case EF_APP:
                 pop_app_frame(static_cast<app_frame*>(fr));
                 break;
-            case EF_LET: 
+            case EF_LET:
                 pop_let_frame(static_cast<let_frame*>(fr));
                 break;
             case EF_LET_DECL:
@@ -1714,7 +1718,7 @@ namespace smt2 {
         void parse_expr() {
             m_num_expr_frames = 0;
             do {
-                TRACE("parse_expr", tout << "curr(): " << curr() << ", m_num_expr_frames: " << m_num_expr_frames 
+                TRACE("parse_expr", tout << "curr(): " << curr() << ", m_num_expr_frames: " << m_num_expr_frames
                       << ", expr_stack().size(): " << expr_stack().size() << "\n";);
                 if (curr_is_rparen()) {
                     if (m_num_expr_frames == 0)
@@ -1798,7 +1802,7 @@ namespace smt2 {
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_declare_sort);
             next();
-            
+
             check_identifier("invalid sort declaration, symbol expected");
             symbol id = curr_id();
             if (m_ctx.find_psort_decl(id) != 0)
@@ -1812,7 +1816,7 @@ namespace smt2 {
                 check_int("invalid sort declaration, arity (<numeral>) or ')' expected");
                 rational n = curr_numeral();
                 if (!n.is_unsigned())
-                    throw parser_exception("invalid sort declaration, arity is too big to fit in an unsigned machine integer");                
+                    throw parser_exception("invalid sort declaration, arity is too big to fit in an unsigned machine integer");
                 psort_decl * decl = pm().mk_psort_user_decl(n.get_unsigned(), id, 0);
                 m_ctx.insert(decl);
                 next();
@@ -1872,12 +1876,12 @@ namespace smt2 {
         }
 
         void parse_define_fun_rec() {
-            // ( define-fun-rec hfun_defi ) 
+            // ( define-fun-rec hfun_defi )
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_define_fun_rec);
             SASSERT(m_num_bindings == 0);
             next();
-            
+
             expr_ref_vector binding(m());
             svector<symbol> ids;
             func_decl_ref f(m());
@@ -1890,7 +1894,7 @@ namespace smt2 {
         }
 
         void parse_define_funs_rec() {
-            // ( define-funs-rec ( hfun_decin+1 ) ( htermin+1 ) ) 
+            // ( define-funs-rec ( hfun_decin+1 ) ( htermin+1 ) )
             SASSERT(curr_is_identifier());
             SASSERT(curr_id() == m_define_funs_rec);
             SASSERT(m_num_bindings == 0);
@@ -1920,14 +1924,14 @@ namespace smt2 {
 
                 check_lparen("invalid recursive function definition, '(' expected");
                 next();
-            
+
                 parse_rec_fun_decl(f, binding, id);
                 decls.push_back(f);
                 bindings.push_back(binding);
                 ids.push_back(id);
 
                 check_rparen("invalid recursive function definition, ')' expected");
-                next();                
+                next();
             }
             next();
         }
@@ -1950,7 +1954,7 @@ namespace smt2 {
             sort_stack().shrink(sort_spos);
             expr_stack().shrink(expr_spos);
             m_env.end_scope();
-            m_num_bindings = 0;            
+            m_num_bindings = 0;
         }
 
         void parse_rec_fun_bodies(func_decl_ref_vector const& decls, vector<expr_ref_vector> const& bindings, vector<svector<symbol> >const & ids) {
@@ -1963,10 +1967,10 @@ namespace smt2 {
             }
 
             if (i != decls.size()) {
-                throw parser_exception("the number of declarations does not match number of supplied definitions");                    
+                throw parser_exception("the number of declarations does not match number of supplied definitions");
             }
             check_rparen("invalid recursive function definition, ')' expected");
-            next();                
+            next();
         }
 
         void parse_rec_fun_body(func_decl* f, expr_ref_vector const& bindings, svector<symbol> const& ids) {
@@ -1980,19 +1984,19 @@ namespace smt2 {
             for (unsigned i = 0; i < num_vars; ++i) {
                 m_env.insert(ids[i], local(bindings[i], num_vars));
             }
-            parse_expr();            
+            parse_expr();
             body = expr_stack().back();
             expr_stack().pop_back();
             symbol_stack().shrink(sym_spos);
             m_env.end_scope();
-            m_num_bindings = 0;            
+            m_num_bindings = 0;
             if (m().get_sort(body) != f->get_range()) {
                 std::ostringstream buffer;
                 buffer << "invalid function definition, sort mismatch. Expcected "
-                       << mk_pp(f->get_range(), m()) << " but function body has sort " 
+                       << mk_pp(f->get_range(), m()) << " but function body has sort "
                        << mk_pp(m().get_sort(body), m());
                 throw parser_exception(buffer.str().c_str());
-            } 
+            }
             m_ctx.insert_rec_fun(f, bindings, ids, body);
         }
 
@@ -2185,7 +2189,7 @@ namespace smt2 {
             unsigned spos = expr_stack().size();
             check_lparen_next("invalid check-sat-assuming command, '(', expected");
             parse_assumptions();
-            check_rparen_next("invalid check-sat-assuming command, ')', expected");            
+            check_rparen_next("invalid check-sat-assuming command, ')', expected");
             m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos);
             next();
             expr_stack().shrink(spos);
@@ -2201,7 +2205,7 @@ namespace smt2 {
             m_scanner.start_caching();
             m_cache_end = 0;
             m_cached_strings.resize(0);
-            
+
             check_lparen_next("invalid get-value command, '(' expected");
             while (!curr_is_rparen()) {
                 parse_expr();
@@ -2241,7 +2245,7 @@ namespace smt2 {
             SASSERT(curr_id() == m_reset);
             next();
             check_rparen("invalid reset command, ')' expected");
-            m_ctx.reset(); 
+            m_ctx.reset();
             reset();
             m_ctx.print_success();
             next();
@@ -2323,7 +2327,7 @@ namespace smt2 {
             }
             next();
         }
-        
+
         void parse_next_cmd_arg() {
             SASSERT(m_curr_cmd != 0);
             cmd_arg_kind k = m_curr_cmd->next_arg_kind(m_ctx);
@@ -2332,7 +2336,7 @@ namespace smt2 {
                 check_int("invalid command argument, unsigned integer expected");
                 rational n = curr_numeral();
                 if (!n.is_unsigned())
-                    throw parser_exception("invalid command argument, numeral is too big to fit in an unsigned machine integer"); 
+                    throw parser_exception("invalid command argument, numeral is too big to fit in an unsigned machine integer");
                 m_curr_cmd->set_next_arg(m_ctx, n.get_unsigned());
                 next();
                 break;
@@ -2445,7 +2449,7 @@ namespace smt2 {
             m_curr_cmd = m_ctx.find_cmd(s);
             if (m_curr_cmd == 0) {
                 parse_unknown_cmd();
-                return; 
+                return;
             }
             next();
             unsigned arity = m_curr_cmd->get_arity();
@@ -2475,14 +2479,14 @@ namespace smt2 {
                     return;
                 }
                 else {
-                    if (arity != VAR_ARITY && i == arity) 
+                    if (arity != VAR_ARITY && i == arity)
                         throw parser_exception("invalid command, too many arguments");
                     parse_next_cmd_arg();
                 }
                 i++;
             }
         }
-        
+
         void parse_cmd() {
             SASSERT(curr_is_lparen());
             int line = m_scanner.get_line();
@@ -2531,7 +2535,7 @@ namespace smt2 {
                 return;
             }
             if (s == m_declare_datatypes) {
-                parse_declare_datatypes(); 
+                parse_declare_datatypes();
                 return;
             }
             if (s == m_get_value) {
@@ -2558,8 +2562,8 @@ namespace smt2 {
         }
 
     public:
-        parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
-            m_ctx(ctx), 
+        parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p, char const * filename=0):
+            m_ctx(ctx),
             m_params(p),
             m_scanner(ctx, is, interactive),
             m_curr(scanner::NULL_TOKEN),
@@ -2597,14 +2601,15 @@ namespace smt2 {
             m_check_sat_assuming("check-sat-assuming"),
             m_define_fun_rec("define-fun-rec"),
             m_define_funs_rec("define-funs-rec"),
-            m_underscore("_"),            
-            m_num_open_paren(0) {
+            m_underscore("_"),
+            m_num_open_paren(0),
+            m_current_file(filename) {
             // the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
             // SASSERT(!m_ctx.has_manager());
-            
+
             updt_params();
         }
-        
+
         ~parser() {
             reset_stack();
         }
@@ -2615,7 +2620,7 @@ namespace smt2 {
             m_ignore_bad_patterns  = p.ignore_bad_patterns();
             m_display_error_for_vs = p.error_for_visual_studio();
         }
-  
+
         void reset() {
             reset_stack();
             m_num_bindings    = 0;
@@ -2630,7 +2635,7 @@ namespace smt2 {
             m_env               .reset();
             m_sort_id2param_idx .reset();
             m_dt_name2idx       .reset();
-            
+
             m_bv_util           = 0;
             m_arith_util        = 0;
             m_seq_util          = 0;
@@ -2680,9 +2685,9 @@ namespace smt2 {
                     return !found_errors;
                 }
                 catch (parser_exception & ex) {
-                    if (ex.has_pos()) 
+                    if (ex.has_pos())
                         error(ex.line(), ex.pos(), ex.msg());
-                    else 
+                    else
                         error(ex.msg());
                 }
                 catch (ast_exception & ex) {
@@ -2705,8 +2710,8 @@ namespace smt2 {
     };
 };
 
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps) {
-    smt2::parser p(ctx, is, interactive, ps);
+bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
+    smt2::parser p(ctx, is, interactive, ps, filename);
     return p();
 }
 
diff --git a/src/parsers/smt2/smt2parser.h b/src/parsers/smt2/smt2parser.h
index 5b4384917..77fd41d5d 100644
--- a/src/parsers/smt2/smt2parser.h
+++ b/src/parsers/smt2/smt2parser.h
@@ -21,6 +21,6 @@ Revision History:
 
 #include"cmd_context.h"
 
-bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref());
+bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref(), char const * filename = 0);
 
 #endif

From e472a8d4cfe36df6a68d0b4e285e9a3410d6ff8a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Jan 2017 15:46:58 +0000
Subject: [PATCH 4/7] Enabled filenames in error messages during inclusion of
 files.

---
 src/smt/smt2_extra_cmds.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt2_extra_cmds.cpp b/src/smt/smt2_extra_cmds.cpp
index 866a1178e..901810442 100644
--- a/src/smt/smt2_extra_cmds.cpp
+++ b/src/smt/smt2_extra_cmds.cpp
@@ -34,7 +34,7 @@ public:
         std::ifstream is(m_filename);
         if (is.bad() || is.fail())
             throw cmd_exception(std::string("failed to open file '") + m_filename + "'");
-        parse_smt2_commands(ctx, is, false);
+        parse_smt2_commands(ctx, is, false, params_ref(), m_filename);
         is.close();
     }
     virtual void prepare(cmd_context & ctx) { reset(ctx); }

From 625681f82f3ac3e86c4fe6755c4939bf477af6f7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Jan 2017 15:59:16 +0000
Subject: [PATCH 5/7] Updated cmake build

---
 contrib/cmake/src/smt/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/contrib/cmake/src/smt/CMakeLists.txt
index 035ac07c9..bd8ad3f31 100644
--- a/contrib/cmake/src/smt/CMakeLists.txt
+++ b/contrib/cmake/src/smt/CMakeLists.txt
@@ -43,6 +43,7 @@ z3_add_component(smt
     smt_statistics.cpp
     smt_theory.cpp
     smt_value_sort.cpp
+    smt2_extra_cmds.cpp
     theory_arith.cpp
     theory_array_base.cpp
     theory_array.cpp

From 0fae048e3e00f380bea70cb863625097f4854a46 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 17 Jan 2017 12:58:32 +0000
Subject: [PATCH 6/7] Windows build fix.

---
 scripts/mk_win_dist.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
index eb9f707a2..11048650f 100644
--- a/scripts/mk_win_dist.py
+++ b/scripts/mk_win_dist.py
@@ -316,7 +316,7 @@ def main():
         mk_dist_dirs()
         cp_licenses()
         cp_vs_runtimes()
-        mk_zip()
+        mk_zips()
 
 main()
 

From 6d34899c463db50cf4248c6e4f2451e6003919e7 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 17 Jan 2017 15:44:03 +0000
Subject: [PATCH 7/7] Bugfix for macro finder. Fixes #832.

---
 src/ast/macros/macro_manager.cpp | 18 +++++------
 src/ast/macros/macro_util.cpp    | 51 ++++++++++++++++----------------
 src/ast/macros/macro_util.h      | 16 +++++-----
 3 files changed, 42 insertions(+), 43 deletions(-)

diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 75b4e55f4..b17e1ce28 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -106,7 +106,7 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
     if (!m_deps.insert(f, s)) {
         return false;
     }
-    
+
     // add macro
     m_decl2macro.insert(f, m);
     m_decls.push_back(f);
@@ -117,8 +117,8 @@ bool macro_manager::insert(func_decl * f, quantifier * m, proof * pr) {
     }
 
     TRACE("macro_insert", tout << "A macro was successfully created for: " << f->get_name() << "\n";);
-    
-    // Nothing's forbidden anymore; if something's bad, we detected it earlier. 
+
+    // Nothing's forbidden anymore; if something's bad, we detected it earlier.
     // mark_forbidden(m->get_expr());
     return true;
 }
@@ -144,7 +144,7 @@ namespace macro_manager_ns {
    \brief Mark all func_decls used in exprs as forbidden.
 */
 void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) {
-    expr_mark visited; 
+    expr_mark visited;
     macro_manager_ns::proc p(m_forbidden_set, m_forbidden);
     for (unsigned i = 0; i < n; i++)
         for_each_expr(p, visited, exprs[i]);
@@ -187,9 +187,9 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
     app * head;
     expr * def;
     get_head_def(q, f, head, def);
-    TRACE("macro_bug", 
+    TRACE("macro_bug",
           tout << f->get_name() << "\n" << mk_pp(head, m_manager) << "\n" << mk_pp(q, m_manager) << "\n";);
-    m_util.mk_macro_interpretation(head, def, interp);
+    m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp);
     return f;
 }
 
@@ -237,7 +237,7 @@ void macro_manager::macro_expander::reduce1_quantifier(quantifier * q) {
                 erase_patterns = true;
         }
         for (unsigned i = 0; !erase_patterns && i < q->get_num_no_patterns(); i++) {
-            if (q->get_no_pattern(i) != new_q->get_no_pattern(i)) 
+            if (q->get_no_pattern(i) != new_q->get_no_pattern(i))
                 erase_patterns = true;
         }
     }
@@ -254,7 +254,7 @@ bool macro_manager::macro_expander::get_subst(expr * _n, expr_ref & r, proof_ref
         return false;
     app * n = to_app(_n);
     quantifier * q = 0;
-    func_decl * d  = n->get_decl(); 
+    func_decl * d  = n->get_decl();
     TRACE("macro_manager_bug", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
     if (m_macro_manager.m_decl2macro.find(d, q)) {
         TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
@@ -308,7 +308,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_ref & r, proof_ref
             if (r.get() == old_n.get())
                 return;
             old_n  = r;
-            old_pr = new_pr; 
+            old_pr = new_pr;
         }
     }
     else {
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 97b44d4cd..99732871c 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -405,7 +405,7 @@ bool macro_util::is_quasi_macro_head(expr * n, unsigned num_decls) const {
    \brief Convert a quasi-macro head into a macro head, and store the conditions under
    which it is valid in cond.
 */
-void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const {
+void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const {
     unsigned num_args = qhead->get_num_args();
     sbuffer<bool> found_vars;
     found_vars.resize(num_decls, false);
@@ -431,6 +431,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls,
     }
     get_basic_simp()->mk_and(new_conds.size(), new_conds.c_ptr(), cond);
     head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.c_ptr());
+    num_decls = next_var_idx;
 }
 
 /**
@@ -440,10 +441,10 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls,
 
    See normalize_expr
 */
-void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & interp) const {
+void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
     SASSERT(is_macro_head(head, head->get_num_args()));
     SASSERT(!occurs(head->get_decl(), def));
-    normalize_expr(head, def, interp);
+    normalize_expr(head, num_decls, def, interp);
 }
 
 /**
@@ -456,36 +457,27 @@ void macro_util::mk_macro_interpretation(app * head, expr * def, expr_ref & inte
    f(x_1, x_2) --> f(x_0, x_1)
    f(x_3, x_2) --> f(x_0, x_1)
 */
-void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
-    expr_ref_buffer  var_mapping(m_manager);
+void macro_util::normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const {
+    expr_ref_buffer var_mapping(m_manager);
+    var_mapping.resize(num_decls);
     bool changed = false;
     unsigned num_args = head->get_num_args();
-    unsigned max_var_idx = 0;
-    for (unsigned i = 0; i < num_args; i++) {
-        var const * v = to_var(head->get_arg(i));
-        if (v->get_idx() > max_var_idx)
-            max_var_idx = v->get_idx();
-    }
     TRACE("macro_util",
           tout << "head: " << mk_pp(head, m_manager) << "\n";
           tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";);
     for (unsigned i = 0; i < num_args; i++) {
         var * v = to_var(head->get_arg(i));
-        if (v->get_idx() != i) {
+        unsigned vi = v->get_idx();
+        SASSERT(vi < num_decls);
+        if (vi != i) {
             changed = true;
             var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager);
-            var_mapping.setx(max_var_idx - v->get_idx(), new_var);
+            var_mapping.setx(num_decls - vi - 1, new_var);
         }
         else
-            var_mapping.setx(max_var_idx - i, v);
+            var_mapping.setx(num_decls - i - 1, v);
     }
 
-    for (unsigned i = num_args; i <= max_var_idx; i++)
-        // CMW: Won't be used, but dictates a larger binding size,
-        // so that the indexes between here and in the rewriter match.
-        // It's possible that we don't see the true max idx of all vars here.
-        var_mapping.setx(max_var_idx - i, 0);
-
     if (changed) {
         // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
         var_subst subst(m_manager, true);
@@ -573,7 +565,7 @@ bool is_hint_atom(expr * lhs, expr * rhs) {
     return !occurs(to_app(lhs)->get_decl(), rhs) && vars_of_is_subset(rhs, vars);
 }
 
-void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref & new_head) {
+void hint_to_macro_head(ast_manager & m, app * head, unsigned & num_decls, app_ref & new_head) {
     unsigned num_args = head->get_num_args();
     ptr_buffer<expr> new_args;
     sbuffer<bool> found_vars;
@@ -595,6 +587,7 @@ void hint_to_macro_head(ast_manager & m, app * head, unsigned num_decls, app_ref
         new_args.push_back(new_var);
     }
     new_head = m.mk_app(head->get_decl(), new_args.size(), new_args.c_ptr());
+    num_decls = next_var_idx;
 }
 
 /**
@@ -671,12 +664,12 @@ void macro_util::macro_candidates::insert(func_decl * f, expr * def, expr * cond
 //
 // -----------------------------
 
-void macro_util::insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) {
+void macro_util::insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r) {
     expr_ref norm_def(m_manager);
     expr_ref norm_cond(m_manager);
-    normalize_expr(head, def, norm_def);
+    normalize_expr(head, num_decls, def, norm_def);
     if (cond != 0)
-        normalize_expr(head, cond, norm_cond);
+        normalize_expr(head, num_decls, cond, norm_cond);
     else if (!hint)
         norm_cond = m_manager.mk_true();
     SASSERT(!hint || norm_cond.get() == 0);
@@ -698,11 +691,14 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def,
         }
         else {
             hint_to_macro_head(m_manager, head, num_decls, new_head);
+            TRACE("macro_util",
+                tout << "hint macro head: " << mk_ismt2_pp(new_head, m_manager) << std::endl;
+                tout << "hint macro def: " << mk_ismt2_pp(def, m_manager) << std::endl; );
         }
-        insert_macro(new_head, def, new_cond, ineq, satisfy_atom, hint, r);
+        insert_macro(new_head, num_decls, def, new_cond, ineq, satisfy_atom, hint, r);
     }
     else {
-        insert_macro(head, def, cond, ineq, satisfy_atom, hint, r);
+        insert_macro(head, num_decls, def, cond, ineq, satisfy_atom, hint, r);
     }
 }
 
@@ -879,6 +875,9 @@ void macro_util::collect_arith_macro_candidates(expr * atom, unsigned num_decls,
 */
 void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls, macro_candidates & r) {
     expr* lhs, *rhs;
+
+    TRACE("macro_util", tout << "Candidate check for: " << mk_ismt2_pp(atom, m_manager) << std::endl;);
+
     if (m_manager.is_eq(atom, lhs, rhs) || m_manager.is_iff(atom, lhs, rhs)) {
         if (is_quasi_macro_head(lhs, num_decls) &&
             !is_forbidden(to_app(lhs)->get_decl()) &&
diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h
index 18b00c1f7..033f6ecb4 100644
--- a/src/ast/macros/macro_util.h
+++ b/src/ast/macros/macro_util.h
@@ -74,9 +74,9 @@ private:
     void collect_arith_macros(expr * n, unsigned num_decls, unsigned max_macros, bool allow_cond_macros,
                               macro_candidates & r);
 
-    void normalize_expr(app * head, expr * t, expr_ref & norm_t) const;
-    void insert_macro(app * head, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r);
-    void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, 
+    void normalize_expr(app * head, unsigned num_decls, expr * t, expr_ref & norm_t) const;
+    void insert_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, macro_candidates & r);
+    void insert_quasi_macro(app * head, unsigned num_decls, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint,
                             macro_candidates & r);
 
     expr * m_curr_clause; // auxiliary var used in collect_macro_candidates.
@@ -105,7 +105,7 @@ public:
     bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
     bool is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const;
     bool is_simple_macro(expr * n, unsigned num_decls, app_ref& head, expr_ref & def) const {
-        return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def); 
+        return is_left_simple_macro(n, num_decls, head, def) || is_right_simple_macro(n, num_decls, head, def);
     }
 
     bool is_arith_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def, bool & inv) const;
@@ -113,20 +113,20 @@ public:
         bool inv;
         return is_arith_macro(n, num_decls, head, def, inv);
     }
-    
+
     bool is_pseudo_head(expr * n, unsigned num_decls, app_ref & head, app_ref & t);
     bool is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t, expr_ref & def);
 
     bool is_quasi_macro_head(expr * n, unsigned num_decls) const;
-    void quasi_macro_head_to_macro_head(app * qhead, unsigned num_decls, app_ref & head, expr_ref & cond) const;
+    void quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decls, app_ref & head, expr_ref & cond) const;
 
-    void mk_macro_interpretation(app * head, expr * def, expr_ref & interp) const;
+    void mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const;
 
     void collect_macro_candidates(expr * atom, unsigned num_decls, macro_candidates & r);
     void collect_macro_candidates(quantifier * q, macro_candidates & r);
 
     //
-    // Auxiliary goodness that allows us to manipulate BV and Arith polynomials. 
+    // Auxiliary goodness that allows us to manipulate BV and Arith polynomials.
     //
     bool is_bv(expr * n) const;
     bool is_bv_sort(sort * s) const;