From 3ca85913476fc71d515518e178dd2ae8787b386c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Jul 2014 09:59:35 -0700
Subject: [PATCH 01/42] take theory explanation into account

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 02ee06985..4f3c73ce6 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3945,7 +3945,7 @@ namespace smt {
               m_fingerprints.display(tout); 
               );
         failure fl = get_last_search_failure();
-        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
+        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
             // don't generate model.
             return;
         }

From 06a4a3599da0fd89479f30e30f4aaea46bff47f9 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 29 Jul 2014 18:04:54 +0100
Subject: [PATCH 02/42] Added git hashcode information to (get-info :version)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/cmd_context/basic_cmds.cpp | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 527230e16..836ade9ce 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -547,6 +547,9 @@ public:
     }
 };
 
+#define STRINGIZE(x) #x
+#define STRINGIZE_VALUE_OF(x) STRINGIZE(x)
+
 class get_info_cmd : public cmd {
     symbol   m_error_behavior;
     symbol   m_name;
@@ -584,7 +587,11 @@ public:
             ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl;
         }
         else if (opt == m_version) {
-            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl;
+            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
+#ifdef Z3GITHASH
+                << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH)
+#endif
+                << "\")" << std::endl;
         }
         else if (opt == m_status) {
             ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;

From 39646bac3e58d8a28c0c5abc818d28b054b3a4bb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 31 Jul 2014 16:32:25 +0100
Subject: [PATCH 03/42] added operator[] to obj_map for convenience

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/util/obj_hashtable.h | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 603898af8..8ff5f8e8f 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -165,6 +165,14 @@ public:
         SASSERT(e);
         return e->get_data().m_value;
     }
+
+    value const & operator[](key * k) const {
+        return find(k);
+    }
+
+    value & operator[](key * k) {
+        return find(k);
+    }
     
     iterator find_iterator(Key * k) const { 
         return m_table.find(key_data(k));

From 7bf87e76eaec6ae7cd59b52f7a3c775062d13562 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 5 Aug 2014 11:11:43 -0700
Subject: [PATCH 04/42] fix for tree interpolation

---
 src/interp/iz3interp.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index bed93a56f..1ae3e3a1b 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -347,8 +347,10 @@ public:
     // get the interps for the tree positions
     std::vector<ast> _interps = interps;
     interps.resize(pos_map.size());
-    for(unsigned i = 0; i < pos_map.size(); i++)
-      interps[i] = i < _interps.size() ? _interps[i] : mk_false();
+    for(unsigned i = 0; i < pos_map.size(); i++){
+      unsigned j = pos_map[i];
+      interps[i] = j < _interps.size() ? _interps[j] : mk_false();
+    }
   }
 
   bool has_interp(hash_map<ast,bool> &memo, const ast &t){

From c007a5e5bde7dae458c1dd8b5a7d131f94edc292 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 11:16:06 -0700
Subject: [PATCH 05/42] merged with unstable

---
 examples/tptp/tptp5.cpp                       |   4 +-
 scripts/mk_util.py                            | 155 ++++++++++--------
 src/api/dotnet/Fixedpoint.cs                  |  39 +++--
 src/api/python/z3.py                          |  28 +++-
 src/api/z3_api.h                              |   3 +-
 src/ast/ast_smt_pp.cpp                        |  10 +-
 src/ast/dl_decl_plugin.cpp                    |  18 +-
 src/ast/dl_decl_plugin.h                      |   2 +
 src/ast/float_decl_plugin.cpp                 |   2 +-
 src/ast/float_decl_plugin.h                   |  11 +-
 src/ast/fpa/fpa2bv_converter.cpp              |  96 ++++++++---
 src/ast/fpa/fpa2bv_converter.h                |   8 +-
 src/ast/fpa/fpa2bv_rewriter.h                 |  10 +-
 src/ast/macros/quasi_macros.cpp               |  17 +-
 src/ast/macros/quasi_macros.h                 |   1 +
 .../bit_blaster/bit_blaster_rewriter.cpp      |   3 +
 .../bit_blaster/bit_blaster_tpl_def.h         |  10 +-
 src/ast/rewriter/bv_rewriter.cpp              |   1 +
 src/ast/rewriter/float_rewriter.cpp           |  21 ++-
 src/cmd_context/basic_cmds.cpp                |   9 +-
 src/muz/base/dl_rule.cpp                      |   5 +-
 src/muz/base/dl_rule.h                        |   2 +-
 src/muz/base/dl_util.cpp                      |   2 +-
 src/muz/bmc/dl_bmc_engine.cpp                 |  10 +-
 src/muz/transforms/dl_mk_array_blast.cpp      |   2 +-
 src/muz/transforms/dl_mk_bit_blast.cpp        |  14 +-
 src/muz/transforms/dl_mk_coalesce.cpp         |   6 +-
 src/muz/transforms/dl_mk_coi_filter.cpp       |   1 -
 .../dl_mk_quantifier_instantiation.cpp        |   5 +-
 src/muz/transforms/dl_mk_rule_inliner.cpp     |  10 +-
 src/muz/transforms/dl_mk_scale.cpp            |   2 +-
 src/qe/qe.cpp                                 | 115 +++++++++----
 src/qe/qe_arith_plugin.cpp                    |  73 ++++++---
 src/smt/params/preprocessor_params.cpp        |   1 +
 src/smt/params/smt_params_helper.pyg          |   1 +
 src/smt/params/theory_arith_params.cpp        |   1 +
 src/smt/proto_model/datatype_factory.cpp      |  11 +-
 src/smt/smt_context.cpp                       |   2 +-
 src/smt/smt_model_generator.cpp               |   2 +
 src/smt/theory_arith_eq.h                     |   2 +-
 src/smt/theory_bv.cpp                         |   1 +
 src/smt/theory_dl.cpp                         |   7 +-
 src/tactic/arith/bv2int_rewriter.cpp          |   2 +
 src/tactic/core/cofactor_elim_term_ite.cpp    |  54 +++---
 src/tactic/core/cofactor_elim_term_ite.h      |   2 +-
 src/tactic/core/cofactor_term_ite_tactic.cpp  |   3 +-
 src/tactic/filter_model_converter.cpp         |   1 +
 src/util/obj_hashtable.h                      |   8 +
 48 files changed, 537 insertions(+), 256 deletions(-)

diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index d0e174914..00d03a8b0 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1630,10 +1630,8 @@ public:
                 unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
                 std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
                 print_hypotheses(out, hyps);
-                out << ").\n";
+                out << "))).\n";
                 break;                
-                display_inference(out, "lemma", "thm", p);
-                break;           
             }     
             case Z3_OP_PR_UNIT_RESOLUTION:                                 
                 display_inference(out, "unit_resolution", "thm", p);
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 89cabe87e..b73f7a7a8 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1,7 +1,7 @@
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
-# 
-# Auxiliary scripts for generating Makefiles 
+#
+# Auxiliary scripts for generating Makefiles
 # and Visual Studio project files.
 #
 # Author: Leonardo de Moura (leonardo)
@@ -42,7 +42,7 @@ BUILD_DIR='build'
 REV_BUILD_DIR='..'
 SRC_DIR='src'
 EXAMPLE_DIR='examples'
-# Required Components 
+# Required Components
 Z3_DLL_COMPONENT='api_dll'
 PATTERN_COMPONENT='pattern'
 UTIL_COMPONENT='util'
@@ -80,7 +80,7 @@ GPROF=False
 GIT_HASH=False
 
 def check_output(cmd):
-    return subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0].rstrip('\r\n')
+    return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n')
 
 def git_hash():
     try:
@@ -222,7 +222,7 @@ def test_openmp(cc):
     return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0
 
 def find_jni_h(path):
-    for root, dirs, files in os.walk(path): 
+    for root, dirs, files in os.walk(path):
         for f in files:
             if f == 'jni.h':
                 return root
@@ -234,7 +234,7 @@ def check_java():
     global JAR
 
     JDK_HOME = getenv('JDK_HOME', None) # we only need to check this locally.
-    
+
     if is_verbose():
         print("Finding javac ...")
 
@@ -283,7 +283,7 @@ def check_java():
 
     oo = TempFile('output')
     eo = TempFile('errout')
-    try: 
+    try:
         subprocess.call([JAVAC, 'Hello.java', '-verbose'], stdout=oo.fname, stderr=eo.fname)
         oo.commit()
         eo.commit()
@@ -298,7 +298,7 @@ def check_java():
     if JNI_HOME != None:
         if not os.path.exists(os.path.join(JNI_HOME, 'jni.h')):
             raise MKException("Failed to detect jni.h '%s'; the environment variable JNI_HOME is probably set to the wrong path." % os.path.join(JNI_HOME))
-    else:        
+    else:
         # Search for jni.h in the library directories...
         t = open('errout', 'r')
         open_pat = re.compile("\[search path for class files: (.*)\]")
@@ -314,22 +314,22 @@ def check_java():
 
         # ... plus some heuristic ones.
         extra_dirs = []
-                    
-        # For the libraries, even the JDK usually uses a JRE that comes with it. To find the 
+
+        # For the libraries, even the JDK usually uses a JRE that comes with it. To find the
         # headers we have to go a little bit higher up.
         for dir in cdirs:
             extra_dirs.append(os.path.abspath(os.path.join(dir, '..')))
 
         if IS_OSX: # Apparently Apple knows best where to put stuff...
             extra_dirs.append('/System/Library/Frameworks/JavaVM.framework/Headers/')
-    
+
         cdirs[len(cdirs):] = extra_dirs
 
         for dir in cdirs:
             q = find_jni_h(dir)
             if q != False:
                 JNI_HOME = q
-                
+
         if JNI_HOME == None:
             raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
 
@@ -351,7 +351,7 @@ def find_cxx_compiler():
         if test_cxx_compiler(cxx):
             CXX = cxx
             return CXX
-    raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')    
+    raise MKException('C++ compiler was not found. Try to set the environment variable CXX with the C++ compiler available in your system.')
 
 def find_c_compiler():
     global CC, C_COMPILERS
@@ -362,7 +362,7 @@ def find_c_compiler():
         if test_c_compiler(c):
             CC = c
             return CC
-    raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')    
+    raise MKException('C compiler was not found. Try to set the environment variable CC with the C compiler available in your system.')
 
 def set_version(major, minor, build, revision):
     global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION
@@ -478,8 +478,8 @@ def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     try:
-        options, remainder = getopt.gnu_getopt(sys.argv[1:], 
-                                               'b:df:sxhmcvtnp:gj', 
+        options, remainder = getopt.gnu_getopt(sys.argv[1:],
+                                               'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
                                                 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
                                                 'githash='])
@@ -534,7 +534,7 @@ def parse_options():
         elif opt == '--gprof':
             GPROF = True
         elif opt == '--githash':
-            GIT_HASH=arg            
+            GIT_HASH=arg
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
@@ -548,7 +548,7 @@ def extract_c_includes(fname):
     system_inc_pat  = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
     # We should generate and error for any occurrence of #include that does not match the previous pattern.
     non_std_inc_pat = re.compile(".*#include.*")
-    
+
     f = open(fname, 'r')
     linenum = 1
     for line in f:
@@ -622,7 +622,7 @@ def is_java_enabled():
     return JAVA_ENABLED
 
 def is_compiler(given, expected):
-    """ 
+    """
     Return True if the 'given' compiler is the expected one.
     >>> is_compiler('g++', 'g++')
     True
@@ -741,7 +741,7 @@ class Component:
         self.add_rule_for_each_include(out, include)
         include_node = '%s.node' % os.path.join(self.build_dir, include)
         out.write('%s: ' % include_node)
-        self.add_cpp_h_deps(out, include)              
+        self.add_cpp_h_deps(out, include)
         out.write('\n')
         out.write('\t@echo done > %s\n' % include_node)
 
@@ -764,7 +764,7 @@ class Component:
         out.write('\n')
         mk_dir(os.path.join(BUILD_DIR, self.build_dir))
         if VS_PAR and IS_WINDOWS:
-            cppfiles = get_cpp_files(self.src_dir)
+            cppfiles = list(get_cpp_files(self.src_dir))
             dependencies = set()
             for cppfile in cppfiles:
                 dependencies.add(os.path.join(self.to_src_dir, cppfile))
@@ -801,7 +801,7 @@ class Component:
     # Return true if the component needs builder to generate an install_tactics.cpp file
     def require_install_tactics(self):
         return False
-    
+
     # Return true if the component needs a def file
     def require_def_file(self):
         return False
@@ -810,6 +810,9 @@ class Component:
     def require_mem_initializer(self):
         return False
 
+    def mk_install_deps(self, out):
+        return
+
     def mk_install(self, out):
         return
 
@@ -818,7 +821,7 @@ class Component:
 
     def is_example(self):
         return False
-    
+
     # Invoked when creating a (windows) distribution package using components at build_path, and
     # storing them at dist_path
     def mk_win_dist(self, build_path, dist_path):
@@ -853,10 +856,13 @@ class LibComponent(Component):
         out.write('\n')
         out.write('%s: %s\n\n' % (self.name, libfile))
 
+    def mk_install_dep(self, out):
+        out.write('%s' % libfile)
+
     def mk_install(self, out):
         for include in self.includes2install:
             out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))
-    
+
     def mk_uninstall(self, out):
         for include in self.includes2install:
             out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'include', include))
@@ -865,7 +871,7 @@ class LibComponent(Component):
         mk_dir(os.path.join(dist_path, 'include'))
         for include in self.includes2install:
             shutil.copy(os.path.join(self.src_dir, include),
-                        os.path.join(dist_path, 'include', include))        
+                        os.path.join(dist_path, 'include', include))
 
     def mk_unix_dist(self, build_path, dist_path):
         self.mk_win_dist(build_path, dist_path)
@@ -935,11 +941,14 @@ class ExeComponent(Component):
     def main_component(self):
         return self.install
 
+    def mk_install_dep(self, out):
+        out.write('%s' % exefile)
+
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
             out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(PREFIX)', 'bin', exefile)))
-    
+
     def mk_uninstall(self, out):
         exefile = '%s$(EXE_EXT)' % self.exe_name
         out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'bin', exefile))
@@ -1063,7 +1072,7 @@ class DLLComponent(Component):
             out.write(' ')
             out.write(obj)
         out.write('\n')
-        
+
     def main_component(self):
         return self.install
 
@@ -1076,6 +1085,11 @@ class DLLComponent(Component):
     def require_def_file(self):
         return IS_WINDOWS and self.export_files
 
+    def mk_install_dep(self, out):
+        out.write('%s$(SO_EXT)' % self.dll_name)
+        if self.static:
+            out.write(' %s$(LIB_EXT)' % self.dll_name)
+
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
@@ -1084,7 +1098,7 @@ class DLLComponent(Component):
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', 'lib', libfile)))
-            
+
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
@@ -1118,7 +1132,7 @@ class DotNetDLLComponent(Component):
         if assembly_info_dir == None:
             assembly_info_dir = "."
         self.dll_name          = dll_name
-        self.assembly_info_dir = assembly_info_dir 
+        self.assembly_info_dir = assembly_info_dir
 
     def mk_makefile(self, out):
         if DOTNET_ENABLED:
@@ -1147,7 +1161,7 @@ class DotNetDLLComponent(Component):
             out.write('\n')
             out.write('%s: %s\n\n' % (self.name, dllfile))
             return
-    
+
     def main_component(self):
         return DOTNET_ENABLED
 
@@ -1180,7 +1194,7 @@ class JavaDLLComponent(Component):
 
         if is_java_enabled():
             mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
-            dllfile = '%s$(SO_EXT)' % self.dll_name            
+            dllfile = '%s$(SO_EXT)' % self.dll_name
             out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
             t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s" -I"%s/PLATFORM" -I%s %s/Native.cpp\n' % (JNI_HOME, JNI_HOME, get_component('api').to_src_dir, self.to_src_dir)
             if IS_OSX:
@@ -1211,16 +1225,16 @@ class JavaDLLComponent(Component):
             JAR = '"%s"' % JAR
             t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes')))
             out.write(t)
-            t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC, 
-                                                  os.path.join('api', 'java', 'classes'), 
-                                                  os.path.join(self.to_src_dir, '*'), 
+            t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC,
+                                                  os.path.join('api', 'java', 'classes'),
+                                                  os.path.join(self.to_src_dir, '*'),
                                                   os.path.join('api', 'java', 'classes')))
             out.write(t)
-            out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name, 
-                                                         os.path.join(self.to_src_dir, 'manifest'), 
+            out.write('\t%s cfm %s.jar %s -C %s .\n' % (JAR, self.package_name,
+                                                         os.path.join(self.to_src_dir, 'manifest'),
                                                          os.path.join('api', 'java', 'classes')))
             out.write('java: %s.jar\n\n' % self.package_name)
-    
+
     def main_component(self):
         return is_java_enabled()
 
@@ -1229,7 +1243,7 @@ class JavaDLLComponent(Component):
             mk_dir(os.path.join(dist_path, 'bin'))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
                         '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
-            shutil.copy(os.path.join(build_path, 'libz3java.dll'), 
+            shutil.copy(os.path.join(build_path, 'libz3java.dll'),
                         os.path.join(dist_path, 'bin', 'libz3java.dll'))
             shutil.copy(os.path.join(build_path, 'libz3java.lib'),
                         os.path.join(dist_path, 'bin', 'libz3java.lib'))
@@ -1240,7 +1254,7 @@ class JavaDLLComponent(Component):
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
                         '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
             so = get_so_ext()
-            shutil.copy(os.path.join(build_path, 'libz3java.%s' % so), 
+            shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
                         os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
 
 class ExampleComponent(Component):
@@ -1296,7 +1310,7 @@ class CExampleComponent(CppExampleComponent):
 
     def src_files(self):
         return get_c_files(self.ex_dir)
-    
+
 class DotNetExampleComponent(ExampleComponent):
     def __init__(self, name, path):
         ExampleComponent.__init__(self, name, path)
@@ -1577,7 +1591,7 @@ def mk_config():
         config.write('CC=%s\n' % CC)
         config.write('CXX=%s\n' % CXX)
         config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))
-        config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)    
+        config.write('EXAMP_DEBUG_FLAG=%s\n' % EXAMP_DEBUG_FLAG)
         config.write('CXX_OUT_FLAG=-o \n')
         config.write('OBJ_EXT=.o\n')
         config.write('LIB_EXT=.a\n')
@@ -1611,7 +1625,11 @@ def mk_config():
                 print('Java Compiler:  %s' % JAVAC)
 
 def mk_install(out):
-    out.write('install:\n')
+    out.write('install: ')
+    for c in get_components():
+        c.mk_install_deps(out)
+        out.write(' ')
+    out.write('\n')
     out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
@@ -1632,7 +1650,7 @@ def mk_install(out):
         out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
                   (os.path.join(PREFIX, 'lib'), LD_LIBRARY_PATH))
         out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
-    out.write('\n')    
+    out.write('\n')
 
 def mk_uninstall(out):
     out.write('uninstall:\n')
@@ -1642,7 +1660,7 @@ def mk_uninstall(out):
     out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
     out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
-    out.write('\n')    
+    out.write('\n')
 
 # Generate the Z3 makefile
 def mk_makefile():
@@ -1697,7 +1715,7 @@ def mk_makefile():
             print('Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"')
         else:
             print("Type 'cd %s; make' to build Z3" % BUILD_DIR)
-        
+
 # Generate automatically generated source code
 def mk_auto_src():
     if not ONLY_MAKEFILES:
@@ -1783,10 +1801,10 @@ def def_module_params(module_name, export, params, class_name=None, description=
     # Generated accessors
     for param in params:
         if export:
-            out.write('  %s %s() const { return p.%s("%s", g, %s); }\n' % 
+            out.write('  %s %s() const { return p.%s("%s", g, %s); }\n' %
                       (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
         else:
-            out.write('  %s %s() const { return p.%s("%s", %s); }\n' % 
+            out.write('  %s %s() const { return p.%s("%s", %s); }\n' %
                       (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
     out.write('};\n')
     out.write('#endif\n')
@@ -1799,8 +1817,8 @@ def max_memory_param():
 def max_steps_param():
     return ('max_steps', UINT, UINT_MAX, 'maximum number of steps')
 
-PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, 
-                'UINT_MAX' : UINT_MAX, 
+PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL,
+                'UINT_MAX' : UINT_MAX,
                 'max_memory_param' : max_memory_param,
                 'max_steps_param' : max_steps_param,
                 'def_module_params' : def_module_params }
@@ -1815,7 +1833,7 @@ def _execfile(file, globals=globals(), locals=locals()):
 # Execute python auxiliary scripts that generate extra code for Z3.
 def exec_pyg_scripts():
     global CURR_PYG
-    for root, dirs, files in os.walk('src'): 
+    for root, dirs, files in os.walk('src'):
         for f in files:
             if f.endswith('.pyg'):
                 script = os.path.join(root, f)
@@ -1831,7 +1849,7 @@ def mk_pat_db():
     fout.write('char const * g_pattern_database =\n')
     for line in fin:
         fout.write('"%s\\n"\n' % line.strip('\n'))
-    fout.write(';\n')    
+    fout.write(';\n')
     if VERBOSE:
         print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
 
@@ -1847,7 +1865,7 @@ def update_version():
         mk_version_dot_h(major, minor, build, revision)
         mk_all_assembly_infos(major, minor, build, revision)
         mk_def_files()
-        
+
 # Update files with the version number
 def mk_version_dot_h(major, minor, build, revision):
     c = get_component(UTIL_COMPONENT)
@@ -1870,8 +1888,8 @@ def mk_all_assembly_infos(major, minor, build, revision):
                 mk_assembly_info_version(assembly, major, minor, build, revision)
             else:
                 raise MKException("Failed to find assembly info file 'AssemblyInfo' at '%s'" % os.path.join(c.src_dir, c.assembly_info_dir))
-                    
-                
+
+
 # Generate version number in the given 'AssemblyInfo.cs' file using 'AssemblyInfo' as a template.
 def mk_assembly_info_version(assemblyinfo, major, minor, build, revision):
     ver_pat   = re.compile('[assembly: AssemblyVersion\("[\.\d]*"\) *')
@@ -1936,7 +1954,7 @@ def mk_install_tactic_cpp(cnames, path):
                     if not added_include:
                         added_include = True
                         fout.write('#include"%s"\n' % h_file)
-                    try: 
+                    try:
                         exec(line.strip('\n '), globals())
                     except:
                         raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
@@ -1944,7 +1962,7 @@ def mk_install_tactic_cpp(cnames, path):
                     if not added_include:
                         added_include = True
                         fout.write('#include"%s"\n' % h_file)
-                    try: 
+                    try:
                         exec(line.strip('\n '), globals())
                     except:
                         raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
@@ -2128,7 +2146,7 @@ def mk_def_files():
 def cp_z3py_to_build():
     mk_dir(BUILD_DIR)
     # Erase existing .pyc files
-    for root, dirs, files in os.walk(Z3PY_SRC_DIR): 
+    for root, dirs, files in os.walk(Z3PY_SRC_DIR):
         for f in files:
             if f.endswith('.pyc'):
                 rmf(os.path.join(root, f))
@@ -2171,7 +2189,7 @@ def mk_bindings(api_files):
             mk_z3consts_java(api_files)
         _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
         cp_z3py_to_build()
-                          
+
 # Extract enumeration types from API files, and add python definitions.
 def mk_z3consts_py(api_files):
     if Z3PY_SRC_DIR == None:
@@ -2208,7 +2226,7 @@ def mk_z3consts_py(api_files):
             m2 = comment_pat.match(line)
             if m1 or m2:
                 # skip blank lines and comments
-                linenum = linenum + 1 
+                linenum = linenum + 1
             elif mode == SEARCHING:
                 m = typedef_pat.match(line)
                 if m:
@@ -2249,7 +2267,7 @@ def mk_z3consts_py(api_files):
             linenum = linenum + 1
     if VERBOSE:
         print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
-                
+
 
 # Extract enumeration types from z3_api.h, and add .Net definitions
 def mk_z3consts_dotnet(api_files):
@@ -2290,7 +2308,7 @@ def mk_z3consts_dotnet(api_files):
             m2 = comment_pat.match(line)
             if m1 or m2:
                 # skip blank lines and comments
-                linenum = linenum + 1 
+                linenum = linenum + 1
             elif mode == SEARCHING:
                 m = typedef_pat.match(line)
                 if m:
@@ -2373,7 +2391,7 @@ def mk_z3consts_java(api_files):
             m2 = comment_pat.match(line)
             if m1 or m2:
                 # skip blank lines and comments
-                linenum = linenum + 1 
+                linenum = linenum + 1
             elif mode == SEARCHING:
                 m = typedef_pat.match(line)
                 if m:
@@ -2411,7 +2429,7 @@ def mk_z3consts_java(api_files):
                         for k in decls:
                             i = decls[k]
                             if first:
-                               first = False 
+                               first = False
                             else:
                                 efile.write(',\n')
                             efile.write('    %s (%s)' % (k, i))
@@ -2422,7 +2440,7 @@ def mk_z3consts_java(api_files):
                         efile.write('    }\n\n')
                         efile.write('    public static final %s fromInt(int v) {\n' % name)
                         efile.write('        for (%s k: values()) \n' % name)
-                        efile.write('            if (k.intValue == v) return k;\n') 
+                        efile.write('            if (k.intValue == v) return k;\n')
                         efile.write('        return values()[0];\n')
                         efile.write('    }\n\n')
                         efile.write('    public final int toInt() { return this.intValue; }\n')
@@ -2573,16 +2591,17 @@ def mk_vs_proj(name, components):
 def mk_win_dist(build_path, dist_path):
     for c in get_components():
         c.mk_win_dist(build_path, dist_path)
-    # Add Z3Py to lib directory
-    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
+    # Add Z3Py to bin directory
+    print("Adding to %s\n" % dist_path)
+    for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
         shutil.copy(os.path.join(build_path, pyc),
                     os.path.join(dist_path, 'bin', pyc))
 
 def mk_unix_dist(build_path, dist_path):
     for c in get_components():
         c.mk_unix_dist(build_path, dist_path)
-    # Add Z3Py to lib directory
-    for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
+    # Add Z3Py to bin directory
+    for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
         shutil.copy(os.path.join(build_path, pyc),
                     os.path.join(dist_path, 'bin', pyc))
 
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 8c6e6c4c6..3f40b220b 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -269,6 +269,14 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
+        BoolExpr[] ToBoolExprs(ASTVector v) {
+            uint n = v.Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = new BoolExpr(Context, v[i].NativeObject);
+            return res;
+        }
+
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
@@ -278,12 +286,7 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
             }
         }
 
@@ -296,15 +299,27 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
-                uint n = v.Size;
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, v[i].NativeObject);
-                return res;
+                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
             }
         }
 
+        /// <summary>
+        /// Parse an SMT-LIB2 file with fixedpoint rules. 
+        /// Add the rules to the current fixedpoint context. 
+        /// Return the set of queries in the file.
+        /// </summary>                
+	public BoolExpr[] ParseFile(string file) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        }
+
+        /// <summary>
+        /// Similar to ParseFile. Instead it takes as argument a string.
+        /// </summary>                
+
+	public BoolExpr[] ParseString(string s) {
+            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+        }
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 9233a41dc..ce53a4c1f 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a):
             return s
         else:
             if __debug__:
+                _z3_assert(s1.ctx == s.ctx, "context mismatch")
                 _z3_assert(False, "sort mismatch")
     else:
         return s
@@ -1459,9 +1460,18 @@ def And(*args):
     >>> And(P)
     And(p__0, p__1, p__2, p__3, p__4)
     """
-    args  = _get_args(args)
-    ctx   = _ctx_from_ast_arg_list(args)
+    last_arg = None
+    if len(args) > 0:
+        last_arg = args[len(args)-1]
+    if isinstance(last_arg, Context):
+        ctx = args[len(args)-1]
+        args = args[:len(args)-1]
+    else:
+        ctx = main_ctx()
+    args = _get_args(args)
+    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
     if __debug__:
+        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
     if _has_probe(args):
         return _probe_and(args, ctx)
@@ -1480,9 +1490,18 @@ def Or(*args):
     >>> Or(P)
     Or(p__0, p__1, p__2, p__3, p__4)
     """
-    args  = _get_args(args)
-    ctx   = _ctx_from_ast_arg_list(args)
+    last_arg = None
+    if len(args) > 0:
+        last_arg = args[len(args)-1]
+    if isinstance(last_arg, Context):
+        ctx = args[len(args)-1]
+        args = args[:len(args)-1]
+    else:
+        ctx = main_ctx()
+    args = _get_args(args)
+    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
     if __debug__:
+        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
     if _has_probe(args):
         return _probe_or(args, ctx)
@@ -4128,6 +4147,7 @@ class Datatype:
         """
         if __debug__:
             _z3_assert(isinstance(name, str), "String expected")
+            _z3_assert(name != "", "Constructor name cannot be empty")
         return self.declare_core(name, "is_" + name, *args)
 
     def __repr__(self):
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b29a9c87d..94e20eceb 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5668,7 +5668,8 @@ END_MLAPI_EXCLUDE
        Each conjunct encodes values of the bound variables of the query that are satisfied.
        In PDR mode, the returned answer is a single conjunction.
 
-       The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+       When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+       When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
 
        def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
     */    
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f684879ae..59e5c04b9 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -569,8 +569,8 @@ class smt_printer {
             m_out << ")";
         }
         
-        if (m_is_smt2 && q->get_num_patterns() > 0) {
-            m_out << "(!";
+        if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
+            m_out << "(! ";
         }
         {
             smt_printer p(m_out, m_manager, m_qlists, m_renaming, m_logic, false, m_is_smt2, m_simplify_implies, m_indent, m_num_var_names, m_var_names);        
@@ -609,7 +609,11 @@ class smt_printer {
                 m_out << "}";
             }
         }
-        if (m_is_smt2 && q->get_num_patterns() > 0) {
+
+        if (q->get_qid() != symbol::null)
+            m_out << " :qid " << q->get_qid();
+
+        if (m_is_smt2 && (q->get_num_patterns() > 0 || q->get_qid() != symbol::null)) {
             m_out << ")";
         }
         m_out << ")";
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index 6d0823a24..badf8a59d 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -599,7 +599,23 @@ namespace datalog {
                         return 0;
                 }
                 result = mk_compare(OP_DL_LT, m_lt_sym, domain);
-                break;                
+                break;   
+
+            case OP_DL_REP: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
+                break;
+            }
+                
+            case OP_DL_ABS: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
+                break;
+            }
 
             default:
                 m_manager->raise_exception("operator not recognized");
diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h
index a662de578..65b00235c 100644
--- a/src/ast/dl_decl_plugin.h
+++ b/src/ast/dl_decl_plugin.h
@@ -48,6 +48,8 @@ namespace datalog {
         OP_RA_CLONE,
         OP_DL_CONSTANT,
         OP_DL_LT,
+        OP_DL_REP,
+        OP_DL_ABS,
         LAST_RA_OP
     };
     
diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp
index 1adedb2d7..df26422c8 100644
--- a/src/ast/float_decl_plugin.cpp
+++ b/src/ast/float_decl_plugin.cpp
@@ -106,7 +106,7 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
     return false;
 }
 
-bool float_decl_plugin::is_rm(expr * n, mpf_rounding_mode & val) {
+bool float_decl_plugin::is_rm_value(expr * n, mpf_rounding_mode & val) {
     if (is_app_of(n, m_family_id, OP_RM_NEAREST_TIES_TO_AWAY)) {
         val = MPF_ROUND_NEAREST_TAWAY;
         return true;
diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h
index 3786b76ee..58c37080d 100644
--- a/src/ast/float_decl_plugin.h
+++ b/src/ast/float_decl_plugin.h
@@ -169,7 +169,8 @@ public:
     app * mk_value(mpf const & v);
     bool is_value(expr * n) { return is_app_of(n, m_family_id, OP_FLOAT_VALUE); }
     bool is_value(expr * n, mpf & val);
-    bool is_rm(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n, mpf_rounding_mode & val);
+    bool is_rm_value(expr * n) { mpf_rounding_mode t; return is_rm_value(n, t); }
 
     mpf const & get_value(unsigned id) const { 
         SASSERT(m_value_table.contains(id));
@@ -198,7 +199,9 @@ public:
     sort * mk_float_sort(unsigned ebits, unsigned sbits);
     sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
     bool is_float(sort * s) { return is_sort_of(s, m_fid, FLOAT_SORT); }
-    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }    
+    bool is_rm(sort * s) { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
+    bool is_float(expr * e) { return is_float(m_manager.get_sort(e)); }
+    bool is_rm(expr * e) { return is_rm(m_manager.get_sort(e)); }
     unsigned get_ebits(sort * s);
     unsigned get_sbits(sort * s);
 
@@ -217,8 +220,8 @@ public:
 
     app * mk_value(mpf const & v) { return m_plugin->mk_value(v); }
     bool is_value(expr * n) { return m_plugin->is_value(n); }
-    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }    
-    bool is_rm(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm(n, v); }
+    bool is_value(expr * n, mpf & v) { return m_plugin->is_value(n, v); }     
+    bool is_rm_value(expr * n, mpf_rounding_mode & v) { return m_plugin->is_rm_value(n, v); }
 
     app * mk_pzero(unsigned ebits, unsigned sbits);
     app * mk_nzero(unsigned ebits, unsigned sbits);
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 20925a0f9..d6f362902 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -28,9 +28,10 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m(m),
     m_simp(m),
     m_util(m),
-    m_mpf_manager(m_util.fm()),
-    m_mpz_manager(m_mpf_manager.mpz_manager()),
     m_bv_util(m),
+    m_arith_util(m),
+    m_mpf_manager(m_util.fm()),
+    m_mpz_manager(m_mpf_manager.mpz_manager()),    
     extra_assertions(m) {
     m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
 }
@@ -268,7 +269,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
         result = r;
     }
     else {
-        SASSERT(is_rm_sort(f->get_range()));
+        SASSERT(is_rm(f->get_range()));
 
         result = m.mk_fresh_const(
             #ifdef Z3DEBUG
@@ -281,6 +282,10 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
         m_rm_const2bv.insert(f, result);
         m.inc_ref(f);
         m.inc_ref(result);
+
+        expr_ref rcc(m);
+        rcc = bu().mk_ule(result, bu().mk_numeral(4, 3));
+        extra_assertions.push_back(rcc);
     }
 }
 
@@ -1847,6 +1852,55 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         // Just keep it here, as there will be something else that uses it.
         mk_triple(args[0], args[1], args[2], result);
     }
+    else if (num == 3 &&
+             m_bv_util.is_bv(args[0]) &&
+             m_arith_util.is_numeral(args[1]) &&
+             m_arith_util.is_numeral(args[2]))
+    {
+        // Three arguments, some of them are not numerals.
+        SASSERT(m_util.is_float(f->get_range()));
+        unsigned ebits = m_util.get_ebits(f->get_range());
+        unsigned sbits = m_util.get_sbits(f->get_range());
+
+        expr * rm = args[0];
+
+        rational q;
+        if (!m_arith_util.is_numeral(args[1], q))
+            NOT_IMPLEMENTED_YET();
+
+        rational e;
+        if (!m_arith_util.is_numeral(args[2], e))
+            NOT_IMPLEMENTED_YET();
+
+        SASSERT(e.is_int64());
+        SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
+
+        mpf nte, nta, tp, tn, tz;
+        m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator());
+        m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator());
+
+        app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
+        a_nte = m_plugin->mk_value(nte);
+        a_nta = m_plugin->mk_value(nta);
+        a_tp = m_plugin->mk_value(tp);
+        a_tn = m_plugin->mk_value(tn);
+        a_tz = m_plugin->mk_value(tz);
+
+        expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
+        mk_value(a_nte->get_decl(), 0, 0, bv_nte);
+        mk_value(a_nta->get_decl(), 0, 0, bv_nta);
+        mk_value(a_tp->get_decl(), 0, 0, bv_tp);
+        mk_value(a_tn->get_decl(), 0, 0, bv_tn);
+        mk_value(a_tz->get_decl(), 0, 0, bv_tz);
+
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tn, bv_tz, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tp, result, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), bv_nta, result, result);
+        mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), bv_nte, result, result);        
+    }
     else if (num == 1 && m_bv_util.is_bv(args[0])) {
         sort * s = f->get_range();
         unsigned to_sbits = m_util.get_sbits(s);
@@ -1862,7 +1916,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
                   m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
                   result);
     }
-    else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {        
+    else if (num == 2 && 
+             is_app(args[1]) && 
+             m_util.is_float(m.get_sort(args[1]))) {        
         // We also support float to float conversion
         sort * s = f->get_range();
         expr_ref rm(m), x(m); 
@@ -2015,23 +2071,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
             mk_ite(c2, v2, result, result);
             mk_ite(c1, v1, result, result);
         }
-    }
-    else {
+    }    
+    else if (num == 2 &&              
+             m_util.is_rm(args[0]),
+             m_arith_util.is_real(args[1])) {
         // .. other than that, we only support rationals for asFloat
-        SASSERT(num == 2);
         SASSERT(m_util.is_float(f->get_range()));        
         unsigned ebits = m_util.get_ebits(f->get_range());
-        unsigned sbits = m_util.get_sbits(f->get_range());          
-        
-        SASSERT(m_bv_util.is_numeral(args[0]));        
-        rational tmp_rat; unsigned sz; 
-        m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);        
+        unsigned sbits = m_util.get_sbits(f->get_range());
+
+        SASSERT(m_bv_util.is_numeral(args[0]));
+        rational tmp_rat; unsigned sz;
+        m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
         SASSERT(tmp_rat.is_int32());
         SASSERT(sz == 3);
-        BV_RM_VAL bv_rm = (BV_RM_VAL) tmp_rat.get_unsigned();
-        
+        BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
+
         mpf_rounding_mode rm;
-        switch(bv_rm)
+        switch (bv_rm)
         {
         case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
         case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
@@ -2042,22 +2099,23 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
         }
 
         SASSERT(m_util.au().is_numeral(args[1]));
-        
+
         rational q;
-        SASSERT(m_util.au().is_numeral(args[1]));
         m_util.au().is_numeral(args[1], q);
 
         mpf v;
         m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
-    
+
         expr * sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
-        expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits-1);
+        expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
         expr * e = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
 
         mk_triple(sgn, s, e, result);
 
         m_util.fm().del(v);
     }
+    else
+        UNREACHABLE();
 
     SASSERT(is_well_sorted(m, result));    
 }
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 2ccdac6a9..dcb508ffd 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -45,9 +45,10 @@ class fpa2bv_converter {
     ast_manager              & m;
     basic_simplifier_plugin    m_simp;
     float_util                 m_util;
+    bv_util                    m_bv_util;
+    arith_util                 m_arith_util;
     mpf_manager              & m_mpf_manager;
-    unsynch_mpz_manager      & m_mpz_manager;
-    bv_util                    m_bv_util;    
+    unsynch_mpz_manager      & m_mpz_manager;    
     float_decl_plugin        * m_plugin;
 
     obj_map<func_decl, expr*>  m_const2bv;
@@ -64,8 +65,9 @@ public:
 
     bool is_float(sort * s) { return m_util.is_float(s); }
     bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
+    bool is_rm(expr * e) { return m_util.is_rm(e); }
+    bool is_rm(sort * s) { return m_util.is_rm(s); }
     bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
-    bool is_rm_sort(sort * s) { return m_util.is_rm(s); }
 
     void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) {
         SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h
index b2e3da939..225aad668 100644
--- a/src/ast/fpa/fpa2bv_rewriter.h
+++ b/src/ast/fpa/fpa2bv_rewriter.h
@@ -78,17 +78,23 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             return BR_DONE;
         }
 
-        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
+        if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
             m_conv.mk_rm_const(f, result);
             return BR_DONE;
         }
 
         if (m().is_eq(f)) {
             SASSERT(num == 2);
-            if (m_conv.is_float(args[0])) {
+            SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
+            sort * ds = f->get_domain()[0];
+            if (m_conv.is_float(ds)) {
                 m_conv.mk_eq(args[0], args[1], result);
                 return BR_DONE;
             }
+            else if (m_conv.is_rm(ds)) {
+                result = m().mk_eq(args[0], args[1]);
+                return BR_DONE;
+            }
             return BR_FAILED;
         }
 
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index 084a33ebf..b26b7faba 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -41,7 +41,7 @@ void quasi_macros::find_occurrences(expr * e) {
 
     // we remember whether we have seen an expr once, or more than once;
     // when we see it the second time, we don't have to visit it another time,
-    // as we are only intersted in finding unique function applications. 
+    // as we are only interested in finding unique function applications. 
     m_visited_once.reset();
     m_visited_more.reset();
 
@@ -61,7 +61,7 @@ void quasi_macros::find_occurrences(expr * e) {
             case AST_VAR: break;
             case AST_QUANTIFIER: m_todo.push_back(to_quantifier(cur)->get_expr()); break;
             case AST_APP:
-                if (is_uninterp(cur) && !is_ground(cur)) {
+                if (is_non_ground_uninterp(cur)) {
                     func_decl * f = to_app(cur)->get_decl();
                     m_occurrences.insert_if_not_there(f, 0);
                     occurrences_map::iterator it = m_occurrences.find_iterator(f);                    
@@ -76,6 +76,10 @@ void quasi_macros::find_occurrences(expr * e) {
     }
 };
 
+bool quasi_macros::is_non_ground_uninterp(expr const * e) const {
+    return is_non_ground(e) && is_uninterp(e);
+}
+
 bool quasi_macros::is_unique(func_decl * f) const {
     return m_occurrences.find(f) == 1;
 }
@@ -149,6 +153,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
     // Our definition of a quasi-macro:
     // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted, 
     // f[X] contains all universally quantified variables, and f does not occur in T[X].
+    TRACE("quasi_macros", tout << "Checking for quasi macro: " << mk_pp(e, m_manager) << std::endl;);
 
     if (is_quantifier(e) && to_quantifier(e)->is_forall()) {
         quantifier * q = to_quantifier(e);
@@ -157,23 +162,23 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
             expr * lhs = to_app(qe)->get_arg(0);
             expr * rhs = to_app(qe)->get_arg(1);
 
-            if (is_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) && 
+            if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
                 !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
                 a = to_app(lhs);
                 t = rhs;                
                 return true;
-            } else if (is_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) && 
+            } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
                 !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {                
                 a = to_app(rhs);
                 t = lhs;                
                 return true;
             }            
-        } else if (m_manager.is_not(qe) && is_uninterp(to_app(qe)->get_arg(0)) &&
+        } else if (m_manager.is_not(qe) && is_non_ground_uninterp(to_app(qe)->get_arg(0)) &&
                    is_unique(to_app(to_app(qe)->get_arg(0))->get_decl())) { // this is like f(...) = false
             a = to_app(to_app(qe)->get_arg(0));
             t = m_manager.mk_false();
             return true;
-        } else if (is_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
+        } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
             a = to_app(qe);
             t = m_manager.mk_true();
             return true;
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index c5e6b6d4f..64e72e348 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -45,6 +45,7 @@ class quasi_macros {
     expr_mark                 m_visited_more;
     
     bool is_unique(func_decl * f) const;
+    bool is_non_ground_uninterp(expr const * e) const;
     bool fully_depends_on(app * a, quantifier * q) const;    
     bool depends_on(expr * e, func_decl * f) const;
 
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
index 80d319377..63843d31e 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
     
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
+        TRACE("bit_blaster", tout << f->get_name() << " ";
+              for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
+              tout << "\n";);
         if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
             mk_const(f, result);
             return BR_DONE;
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index 72c0a447e..b41aa2238 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
+    TRACE("bit_blaster", tout << n << ": " << sz << " ";
+          for (unsigned i = 0; i < sz; ++i) {
+              tout << mk_pp(a_bits[i], m()) << " ";
+          }
+          tout << "\n";
+          );
     n = n % sz;
     for (unsigned i = sz - n; i < sz; i++) 
         out_bits.push_back(a_bits[i]);
@@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
                 mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
                 out = new_out;
             }
-            TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
+            TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
             out_bits.set(sz - i - 1, out);
         }
     }
@@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             out = a_bits[i];
             for (unsigned j = 1; j < sz; j++) {
                 expr_ref new_out(m());
-                unsigned src = (Left ? (i - j) : (i + j)) % sz;
+                unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
                 mk_ite(eqs.get(j), a_bits[src], out, new_out);
                 out = new_out;
             }
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 11b09003b..1115663d2 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
 
+
 mk_extract_proc::mk_extract_proc(bv_util & u):
     m_util(u),
     m_high(0),
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index ecd06ff38..a4212d579 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@@ -82,7 +82,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
     if (num_args == 2) {
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
         
         rational q;
@@ -109,12 +109,12 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
             return BR_FAILED;
     }
     else if (num_args == 3 && 
-             m_util.is_rm(m().get_sort(args[0])) && 
+             m_util.is_rm(args[0]) && 
              m_util.au().is_real(args[1]) &&
              m_util.au().is_int(args[2])) {
 
         mpf_rounding_mode rm;
-        if (!m_util.is_rm(args[0], rm))
+        if (!m_util.is_rm_value(args[0], rm))
             return BR_FAILED;
 
         rational q;
@@ -129,8 +129,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
         mpf v;
 	    m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
         result = m_util.mk_value(v);
-        m_util.fm().del(v);        
-        // TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
+        m_util.fm().del(v);
         return BR_DONE;
     }
     else {
@@ -140,7 +139,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
 
 br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -161,7 +160,7 @@ br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -176,7 +175,7 @@ br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
             scoped_mpf t(m_util.fm());
@@ -287,7 +286,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
         if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
             scoped_mpf t(m_util.fm());
@@ -302,7 +301,7 @@ br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, exp
 
 br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());
@@ -317,7 +316,7 @@ br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
 
 br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
     mpf_rounding_mode rm;
-    if (m_util.is_rm(arg1, rm)) {
+    if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm());
         if (m_util.is_value(arg2, v2)) {
             scoped_mpf t(m_util.fm());
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 527230e16..836ade9ce 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -547,6 +547,9 @@ public:
     }
 };
 
+#define STRINGIZE(x) #x
+#define STRINGIZE_VALUE_OF(x) STRINGIZE(x)
+
 class get_info_cmd : public cmd {
     symbol   m_error_behavior;
     symbol   m_name;
@@ -584,7 +587,11 @@ public:
             ctx.regular_stream() << "(:authors \"Leonardo de Moura and Nikolaj Bjorner\")" << std::endl;
         }
         else if (opt == m_version) {
-            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "\")" << std::endl;
+            ctx.regular_stream() << "(:version \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER
+#ifdef Z3GITHASH
+                << " - build hashcode " << STRINGIZE_VALUE_OF(Z3GITHASH)
+#endif
+                << "\")" << std::endl;
         }
         else if (opt == m_status) {
             ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 184a5fa02..017bac724 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -978,13 +978,14 @@ namespace datalog {
         }        
     }
 
-    void rule::get_vars(ptr_vector<sort>& sorts) const {
+    void rule::get_vars(ast_manager& m, ptr_vector<sort>& sorts) const {
         sorts.reset();
         used_vars used;
         get_used_vars(used);
         unsigned sz = used.get_max_found_var_idx_plus_1();
         for (unsigned i = 0; i < sz; ++i) {
-            sorts.push_back(used.get(i));
+            sort* s = used.get(i);
+            sorts.push_back(s?s:m.mk_bool_sort());
         }
     }
 
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 1c31dc6b4..7104bae1f 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -304,7 +304,7 @@ namespace datalog {
 
         void norm_vars(rule_manager & rm);
 
-        void get_vars(ptr_vector<sort>& sorts) const;
+        void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
 
         void to_formula(expr_ref& result) const;
 
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 218f9906a..a6647a1d2 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -290,7 +290,7 @@ namespace datalog {
                 }
             }
             TRACE("dl_dr", 
-                  tout << r.get_decl()->get_name() << "\n";
+                  tout << mk_pp(r.get_head(), m) << " :- \n";
                   for (unsigned i = 0; i < body.size(); ++i) {
                       tout << mk_pp(body[i].get(), m) << "\n";
                   });
diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp
index 0dcbf4644..51b1a5295 100644
--- a/src/muz/bmc/dl_bmc_engine.cpp
+++ b/src/muz/bmc/dl_bmc_engine.cpp
@@ -148,7 +148,7 @@ namespace datalog {
         
         void mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
             ptr_vector<sort> sorts;
-            r.get_vars(sorts);
+            r.get_vars(m, sorts);
             // populate substitution of bound variables.
             sub.reset();
             sub.resize(sorts.size());
@@ -421,7 +421,7 @@ namespace datalog {
                     ptr_vector<sort> rule_vars;
                     expr_ref_vector args(m), conjs(m);
 
-                    r.get_vars(rule_vars);
+                    r.get_vars(m, rule_vars);
                     obj_hashtable<expr> used_vars;
                     unsigned num_vars = 0;
                     for (unsigned i = 0; i < r.get_decl()->get_arity(); ++i) {
@@ -514,7 +514,7 @@ namespace datalog {
             unsigned sz = r->get_uninterpreted_tail_size();
 
             ptr_vector<sort> rule_vars;
-            r->get_vars(rule_vars);
+            r->get_vars(m, rule_vars);
             args.append(prop->get_num_args(), prop->get_args());
             expr_ref_vector sub = mk_skolem_binding(*r, rule_vars, args);
             if (sub.empty() && sz == 0) {
@@ -803,7 +803,7 @@ namespace datalog {
             func_decl* p = r.get_decl();
             ptr_vector<func_decl> const& succs  = *dtu.get_datatype_constructors(m.get_sort(path));
             // populate substitution of bound variables.
-            r.get_vars(sorts);
+            r.get_vars(m, sorts);
             sub.reset();
             sub.resize(sorts.size());
             for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
@@ -1327,7 +1327,7 @@ namespace datalog {
         
         void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub) {
             ptr_vector<sort> sorts;
-            r.get_vars(sorts);
+            r.get_vars(m, sorts);
             // populate substitution of bound variables.
             sub.reset();
             sub.resize(sorts.size());
diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 9303181b6..641d40779 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -87,7 +87,7 @@ namespace datalog {
         else {
             if (m_next_var == 0) {
                 ptr_vector<sort> vars;
-                r.get_vars(vars);
+                r.get_vars(m, vars);
                 m_next_var = vars.size() + 1;
             }
             v = m.mk_var(m_next_var, m.get_sort(e));
diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 112541541..fd1dbb205 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -26,6 +26,7 @@ Revision History:
 #include "dl_mk_interp_tail_simplifier.h"
 #include "fixedpoint_params.hpp"
 #include "scoped_proof.h"
+#include "model_v2_pp.h"
 
 namespace datalog {
 
@@ -67,11 +68,17 @@ namespace datalog {
                 func_decl* p = m_new_funcs[i].get();
                 func_decl* q = m_old_funcs[i].get();
                 func_interp* f = model->get_func_interp(p);
+                if (!f) continue;
                 expr_ref body(m);                
                 unsigned arity_p = p->get_arity();
                 unsigned arity_q = q->get_arity();
+                TRACE("dl",
+                      model_v2_pp(tout, *model);
+                      tout << mk_pp(p, m) << "\n";
+                      tout << mk_pp(q, m) << "\n";);
                 SASSERT(0 < arity_p);
-                model->register_decl(p, f);
+                SASSERT(f);
+                model->register_decl(p, f->copy());
                 func_interp* g = alloc(func_interp, m, arity_q);
 
                 if (f) {
@@ -88,11 +95,12 @@ namespace datalog {
                 for (unsigned j = 0; j < arity_q; ++j) {
                     sort* s = q->get_domain(j);
                     arg = m.mk_var(j, s);
+                    expr* t = arg;
                     if (m_bv.is_bv_sort(s)) {
-                        expr* args[1] = { arg };
                         unsigned sz = m_bv.get_bv_size(s);
                         for (unsigned k = 0; k < sz; ++k) {
-                            proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, args);
+                            parameter p(k);
+                            proj = m.mk_app(m_bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t);
                             sub.insert(m.mk_var(idx++, m.mk_bool_sort()), proj); 
                         }
                     }
diff --git a/src/muz/transforms/dl_mk_coalesce.cpp b/src/muz/transforms/dl_mk_coalesce.cpp
index 8c7f1d5b4..ac7a58d8d 100644
--- a/src/muz/transforms/dl_mk_coalesce.cpp
+++ b/src/muz/transforms/dl_mk_coalesce.cpp
@@ -62,7 +62,7 @@ namespace datalog {
         rule_ref r(const_cast<rule*>(&rl), rm);
         ptr_vector<sort> sorts;
         expr_ref_vector revsub(m), conjs(m);
-        rl.get_vars(sorts);
+        rl.get_vars(m, sorts);
         revsub.resize(sorts.size());  
         svector<bool> valid(sorts.size(), true);
         for (unsigned i = 0; i < sub.size(); ++i) {
@@ -117,8 +117,8 @@ namespace datalog {
         rule_ref res(rm);
         bool_rewriter bwr(m);
         svector<bool> is_neg;
-        tgt->get_vars(sorts1);
-        src.get_vars(sorts2);
+        tgt->get_vars(m, sorts1);
+        src.get_vars(m, sorts2);
 
         mk_pred(head, src.get_head(), tgt->get_head()); 
         for (unsigned i = 0; i < src.get_uninterpreted_tail_size(); ++i) {
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index c7a8d5aa0..cdb4a5b9e 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -205,7 +205,6 @@ namespace datalog {
                 for (unsigned i = 0; i < rules.size(); ++i) {
                     app* head = rules[i]->get_head();
                     expr_ref_vector conj(m);
-                    unsigned n = head->get_num_args()-1;
                     for (unsigned j = 0; j < head->get_num_args(); ++j) {
                         expr* arg = head->get_arg(j);
                         if (!is_var(arg)) {
diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
index 9c55ca658..fcb8d7b85 100644
--- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp
@@ -199,7 +199,7 @@ namespace datalog {
         expr_ref fml(m), cnst(m);
         var_ref var(m);
         ptr_vector<sort> sorts;
-        r.get_vars(sorts);
+        r.get_vars(m, sorts);
         m_uf.reset();
         m_terms.reset();
         m_var2cnst.reset();
@@ -207,9 +207,6 @@ namespace datalog {
         fml = m.mk_and(conjs.size(), conjs.c_ptr());
 
         for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (!sorts[i]) {
-                sorts[i] = m.mk_bool_sort();
-            }
             var = m.mk_var(i, sorts[i]);
             cnst = m.mk_fresh_const("C", sorts[i]);
             m_var2cnst.insert(var, cnst);
diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index d9dad5c56..522bd2e86 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -143,11 +143,8 @@ namespace datalog {
         expr_ref_vector result(m);
         ptr_vector<sort> sorts;
         expr_ref v(m), w(m);
-        r.get_vars(sorts);
+        r.get_vars(m, sorts);
         for (unsigned i = 0; i < sorts.size(); ++i) {
-            if (!sorts[i]) {
-                sorts[i] = m.mk_bool_sort();
-            }
             v = m.mk_var(i, sorts[i]);
             m_subst.apply(2, m_deltas, expr_offset(v, is_tgt?0:1), w);
             result.push_back(w);            
@@ -423,6 +420,11 @@ namespace datalog {
         }
 
         TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules;  );
+
+        for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
+            rule* r = m_inlined_rules.get_rule(i);
+            datalog::del_rule(m_mc, *r);
+        }
     }
 
     bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {
diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp
index 9ada7be20..271bf5f62 100644
--- a/src/muz/transforms/dl_mk_scale.cpp
+++ b/src/muz/transforms/dl_mk_scale.cpp
@@ -141,7 +141,7 @@ namespace datalog {
             m_cache.reset();
             m_trail.reset();
             m_eqs.reset();
-            r.get_vars(vars);
+            r.get_vars(m, vars);
             unsigned num_vars = vars.size();
             for (unsigned j = 0; j < utsz; ++j) {
                 tail.push_back(mk_pred(num_vars, r.get_tail(j)));
diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp
index d63f0ae00..770a49c07 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1120,6 +1120,7 @@ namespace qe {
             st->init(fml);
             st->m_vars.append(m_vars.size(), m_vars.c_ptr());
             SASSERT(invariant());
+            TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";);
             return st;
         }
 
@@ -1133,6 +1134,7 @@ namespace qe {
             m_branch_index.insert(branch_id, index);
             st->m_vars.append(m_vars.size(), m_vars.c_ptr());
             SASSERT(invariant());
+            //TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";);
             return st;
         }
 
@@ -1164,6 +1166,16 @@ namespace qe {
             }
         }
 
+        expr_ref abstract_variable(app* x, expr* fml) const {
+            expr_ref result(m);
+            expr* y = x;
+            expr_abstract(m, 0, 1, &y, fml, result);            
+            symbol X(x->get_decl()->get_name());
+            sort* s = m.get_sort(x);
+            result = m.mk_exists(1, &s, &X, result);
+            return result;
+        }
+
         void display_validate(std::ostream& out) const {
             if (m_children.empty()) {
                 return;
@@ -1171,25 +1183,53 @@ namespace qe {
             expr_ref q(m);
             expr* x = m_var;
             if (x) {
-                expr_abstract(m, 0, 1, &x, m_fml, q);
-                ptr_vector<expr> fmls;
+                q = abstract_variable(m_var, m_fml);
+
+                expr_ref_vector fmls(m);
+                expr_ref fml(m);
                 for (unsigned i = 0; i < m_children.size(); ++i) {
-                    expr* fml = m_children[i]->fml();
+                    search_tree const& child = *m_children[i];
+                    fml = child.fml();
                     if (fml) {
+                        // abstract free variables in children.
+                        ptr_vector<app> child_vars, new_vars;
+                        child_vars.append(child.m_vars.size(), child.m_vars.c_ptr());
+                        if (child.m_var) {
+                            child_vars.push_back(child.m_var);
+                        }
+                        for (unsigned j = 0; j < child_vars.size(); ++j) {
+                            if (!m_vars.contains(child_vars[j]) &&
+                                !new_vars.contains(child_vars[j])) {
+                                fml = abstract_variable(child_vars[j], fml);
+                                new_vars.push_back(child_vars[j]);
+                            }
+                        }
                         fmls.push_back(fml);
                     }
                 }
-                symbol X(m_var->get_decl()->get_name());
-                sort* s = m.get_sort(x);
-                q = m.mk_exists(1, &s, &X, q);
-                expr_ref tmp(m);
-                bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), tmp);
-                expr_ref f(m.mk_not(m.mk_iff(q, tmp)), m);
+                bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml);
+                
+                fml = m.mk_not(m.mk_iff(q, fml));
                 ast_smt_pp pp(m);
-                out << "(echo " << m_var->get_decl()->get_name() << ")\n";
+                out << "; eliminate " << mk_pp(m_var, m) << "\n";
                 out << "(push)\n";
-                pp.display_smt2(out, f);
+                pp.display_smt2(out, fml);                
                 out << "(pop)\n\n";      
+                DEBUG_CODE(
+                    smt_params params;
+                    params.m_simplify_bit2int = true;
+                    params.m_arith_enum_const_mod = true;
+                    params.m_bv_enable_int2bv2int = true;
+                    params.m_relevancy_lvl = 0;
+                    smt::kernel ctx(m, params);
+                    ctx.assert_expr(fml);
+                    lbool is_sat = ctx.check();
+                    if (is_sat == l_true) {
+                        std::cout << "; Validation failed:\n";
+                        std::cout << mk_pp(fml, m) << "\n";
+                    }
+);
+
             }
             for (unsigned i = 0; i < m_children.size(); ++i) {
                 if (m_children[i]->fml()) {
@@ -1410,13 +1450,9 @@ namespace qe {
             m_solver.assert_expr(m_fml);
             if (assumption) m_solver.assert_expr(assumption);
             bool is_sat = false;            
-            while (l_false != m_solver.check()) {
+            while (l_true == m_solver.check()) {
                 is_sat = true;
-                model_ref model;
-                m_solver.get_model(model);
-                TRACE("qe", model_v2_pp(tout, *model););
-                model_evaluator model_eval(*model);
-                final_check(model_eval);
+                final_check();
             }
 
             if (!is_sat) {
@@ -1466,14 +1502,30 @@ namespace qe {
 
     private:
 
-        void final_check(model_evaluator& model_eval) {
-            TRACE("qe", tout << "\n";);
-            while (can_propagate_assignment(model_eval)) {
-                propagate_assignment(model_eval);
-            }
-            VERIFY(CHOOSE_VAR == update_current(model_eval, true));
-            SASSERT(m_current->fml());
-            pop(model_eval);        
+        void final_check() {
+            model_ref model;
+            m_solver.get_model(model);
+            scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model);
+
+            while (true) {
+                TRACE("qe", model_v2_pp(tout, *model););
+                while (can_propagate_assignment(*model_eval)) {
+                    propagate_assignment(*model_eval);
+                }
+                VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
+                SASSERT(m_current->fml());
+                if (l_true != m_solver.check()) {
+                    return;
+                }
+                m_solver.get_model(model);
+                model_eval = alloc(model_evaluator, *model);
+                search_tree* st = m_current;
+                update_current(*model_eval, false);
+                if (st == m_current) {
+                    break;
+                }
+            }            
+            pop(*model_eval);                    
         } 
 
         ast_manager& get_manager() { return m; }
@@ -1633,6 +1685,7 @@ namespace qe {
                 nb = m_current->get_num_branches();
                 expr_ref fml(m_current->fml(), m);
                 if (!eval(model_eval, b, branch) || branch >= nb) {
+                    TRACE("qe", tout << "evaluation failed: setting branch to 0\n";);
                     branch = rational::zero();
                 }
                 SASSERT(!branch.is_neg());
@@ -1694,11 +1747,12 @@ namespace qe {
             }
 
             //
-            // The current state is satisfiable
-            // and the closed portion of the formula
-            // can be used as the quantifier-free portion.
+            // The closed portion of the formula
+            // can be used as the quantifier-free portion, 
+            // unless the current state is unsatisfiable.
             // 
             if (m.is_true(fml_mixed)) {
+                SASSERT(l_true == m_solver.check());
                 m_current = m_current->add_child(fml_closed);
                 for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) {
                     expr_ref val(m);
@@ -1708,6 +1762,7 @@ namespace qe {
                     if (val == x) {
                         model_ref model;
                         lbool is_sat = m_solver.check();
+                        if (is_sat == l_undef) return;
                         m_solver.get_model(model);
                         SASSERT(is_sat == l_true);
                         model_evaluator model_eval2(*model);
@@ -1890,7 +1945,7 @@ namespace qe {
                 vars.reset();
                 closed = closed && (r != l_undef);
             }        
-            TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";);
+            TRACE("qe", tout << mk_pp(fml, m) << "\n";);
             m_current->add_child(fml)->reset_free_vars();
             block_assignment(); 
         }
@@ -1959,7 +2014,7 @@ namespace qe {
 
     class quant_elim_new : public quant_elim {
         ast_manager&            m;
-        smt_params&       m_fparams;  
+        smt_params&             m_fparams;  
         expr_ref                m_assumption;
         bool                    m_produce_models;
         ptr_vector<quant_elim_plugin> m_plugins;
diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp
index 7bf0978f6..83c7b79d8 100644
--- a/src/qe/qe_arith_plugin.cpp
+++ b/src/qe/qe_arith_plugin.cpp
@@ -31,6 +31,7 @@ Revision History:
 #include "obj_pair_hashtable.h"
 #include "nlarith_util.h"
 #include "model_evaluator.h"
+#include "smt_kernel.h"
 
 namespace qe {
 
@@ -80,9 +81,9 @@ namespace qe {
         ast_manager&      m;
         i_solver_context& m_ctx;
     public:
-        arith_util                 m_arith; // initialize before m_zero_i, etc.
+        arith_util        m_arith; // initialize before m_zero_i, etc.
+        th_rewriter       simplify;
     private:
-        th_rewriter       m_rewriter;
         arith_eq_solver   m_arith_solver;
         bv_util           m_bv;
 
@@ -102,7 +103,7 @@ namespace qe {
             m(m), 
             m_ctx(ctx),
             m_arith(m),
-            m_rewriter(m),
+            simplify(m),
             m_arith_solver(m),
             m_bv(m),
             m_zero_i(m_arith.mk_numeral(numeral(0), true), m),
@@ -434,7 +435,6 @@ namespace qe {
             expr_ref tmp(e, m);
             simplify(tmp);
             m_arith_rewriter.mk_le(tmp, mk_zero(e), result);
-            TRACE("qe_verbose", tout << "mk_le " << mk_pp(result, m) << "\n";);
         }
 
         void mk_lt(expr* e, expr_ref& result) {
@@ -521,7 +521,8 @@ namespace qe {
                 expr_ref result1(m), result2(m);
                 
                 // a*s + b*t <= 0
-                expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
+                expr_ref as_bt_le_0(result, m), tmp2(m), asz_bt_le_0(m), tmp3(m), tmp4(m);
+                expr_ref b_divides_sz(m);
                 
                 // a*s + b*t + (a-1)(b-1) <= 0
                 tmp2 = m_arith.mk_add(as_bt, slack);
@@ -560,30 +561,36 @@ namespace qe {
                     sz = m_arith.mk_uminus(sz);
                 }
                 tmp4 = mk_add(mk_mul(a1, sz), bt);
-                mk_le(tmp4, tmp3);
+                mk_le(tmp4, asz_bt_le_0);
 
-                if (to_app(tmp3)->get_arg(0) == x &&
-                    m_arith.is_zero(to_app(tmp3)->get_arg(1))) {
+                if (to_app(asz_bt_le_0)->get_arg(0) == x &&
+                    m_arith.is_zero(to_app(asz_bt_le_0)->get_arg(1))) {
                     //    exists z in [0 .. |b|-2] . |b| | (z + s) && z <= 0
                     // <=>
                     //    |b| | s 
                     mk_divides(abs_b, s, tmp2);
                 }
                 else {
-                    mk_divides(abs_b, sz, tmp2);
-                    mk_and(tmp2, tmp3, tmp4);
-                    mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);                                
-                   
+                    mk_divides(abs_b, sz, b_divides_sz);
+                    mk_and(b_divides_sz, asz_bt_le_0, tmp4);
+                    mk_big_or(abs_b - numeral(2), x, tmp4, tmp2);                  
+                    TRACE("qe",
+                          tout << "b | s + z: " << mk_pp(b_divides_sz, m) << "\n";
+                          tout << "a(s+z) + bt <= 0: " << mk_pp(asz_bt_le_0, m) << "\n";
+                          );                   
                 }
                 mk_flat_and(as_bt_le_0, tmp2, result2); 
                 mk_or(result1, result2, result);
                 simplify(result);
+
+
+                //    a*s + b*t + (a-1)(b-1) <= 0 
+                // or exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0
             }
             
             TRACE("qe", 
                   {
-                      expr_ref_vector trail(m);
-                      tout << "is_strict: " << (is_strict?"true":"false") << "\n";
+                      tout << (is_strict?"strict":"non-strict") << "\n";
                       bound(m, a, t, false).pp(tout, x);
                       tout << "\n";
                       bound(m, b, s, false).pp(tout, x);
@@ -592,10 +599,6 @@ namespace qe {
                   });            
         }
         
-        void simplify(expr_ref& p) {
-            m_rewriter(p);
-        }
-
         struct mul_lt {
             arith_util& u;
             mul_lt(arith_qe_util& u): u(u.m_arith) {}
@@ -1052,7 +1055,6 @@ namespace qe {
         }        
 
         bool reduce_equation(expr* p, expr* fml) {
-            TRACE("qe", tout << mk_pp(p, m) << "\n";);
             numeral k;
             
             if (m_arith.is_numeral(p, k) && k.is_zero()) {
@@ -1555,9 +1557,10 @@ public:
                 
                 mk_non_resolve(bounds, true,  is_lower, result);
                 mk_non_resolve(bounds, false, is_lower, result);
+                m_util.simplify(result);
                 add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
                 TRACE("qe", 
-                        tout << vl << " " << mk_pp(x, m) << "\n";
+                        tout << vl << " " << mk_pp(x, m) << " infinite case\n";
                         tout << mk_pp(fml, m) << "\n";
                         tout << mk_pp(result, m) << "\n";);
                 return;
@@ -1591,19 +1594,22 @@ public:
             SASSERT(index < bounds.size(is_strict, is_lower));
             expr_ref t(bounds.exprs(is_strict, is_lower)[index], m);
             rational a = bounds.coeffs(is_strict, is_lower)[index];
+
             
-            t = x_t.mk_term(a, t);
-            a = x_t.mk_coeff(a);
                                 
             mk_bounds(bounds, x, true,  is_eq, is_strict, is_lower, index, a, t, result);
             mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result);
+
+            t = x_t.mk_term(a, t);
+            a = x_t.mk_coeff(a);
             
             mk_resolve(bounds, x, x_t, true,  is_eq, is_strict, is_lower, index, a, t, result);
             mk_resolve(bounds, x, x_t, false, is_eq, is_strict, is_lower, index, a, t, result);
+            m_util.simplify(result);
             add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term());
             TRACE("qe", 
                   {
-                      tout << vl << " " << mk_pp(x, m) << "\n";
+                      tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n";
                       tout << mk_pp(fml, m) << "\n";
                       tout << mk_pp(result, m) << "\n";
                   }
@@ -2225,6 +2231,12 @@ public:
                 }
             }
             m_util.simplify(result);
+            TRACE("qe", 
+                  tout << (is_strict?"strict":"non-strict") << "\n";
+                  tout << (is_lower?"is-lower":"is-upper") << "\n";
+                  tout << "a: " << a << " " << mk_pp(t, m) << "\n";
+                  tout << "b: " << b << " " << mk_pp(s, m) << "\n";
+                  tout << mk_pp(result, m) << "\n";);
         }
 
         //
@@ -2245,10 +2257,12 @@ public:
 
 
         void mk_bounds(bounds_proc& bounds, 
-                       app* x,  bool is_strict, bool is_eq_ctx, bool is_strict_ctx, bool is_lower, unsigned index, 
+                       app* x, bool is_strict, bool is_eq_ctx, 
+                       bool is_strict_ctx, bool is_lower, unsigned index, 
                        rational const& a, expr* t,
                        expr_ref& result) 
         {
+            TRACE("qe", tout << mk_pp(t, m) << "\n";);
             SASSERT(!is_eq_ctx || !is_strict_ctx);
             unsigned sz = bounds.size(is_strict, is_lower);
             expr_ref tmp(m), eq(m);            
@@ -2258,13 +2272,14 @@ public:
 
             for (unsigned i = 0; i < sz; ++i) {
                 app* e   = bounds.atoms(is_strict, is_lower)[i];
-                expr* s  = bounds.exprs(is_strict, is_lower)[i];
+                expr_ref s(bounds.exprs(is_strict, is_lower)[i], m);
                 rational b = bounds.coeffs(is_strict, is_lower)[i]; 
                
                 if (same_strict && i == index) {                    
                     if (non_strict_real) {
                         m_util.mk_eq(a, x, t, eq);
-                        TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << " t: " << mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
+                        TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << "t: " << 
+                              mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";);
                         if (is_eq_ctx) {
                             m_ctx.add_constraint(true, eq);
                         }
@@ -2292,6 +2307,7 @@ public:
                     (non_strict_real && is_eq_ctx && is_strict) ||
                     (same_strict && i < index);
 
+
                 mk_bound(result_is_strict, is_lower, a, t, b, s, tmp);
                 m_util.m_replace.apply_substitution(e, tmp.get(), result);
 
@@ -2330,14 +2346,17 @@ public:
                 s = x_t.mk_term(b, s);
                 b = x_t.mk_coeff(b);
                 m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp);
+                expr_ref save_result(result);
                 m_util.m_replace.apply_substitution(e, tmp.get(), result);
                 
                 m_ctx.add_constraint(true, mk_not(e), tmp);
 
                 TRACE("qe_verbose", 
                       tout << mk_pp(atm, m) << " ";
-                      tout << mk_pp(e, m) << " ==> ";
+                      tout << mk_pp(e, m) << " ==>\n";
                       tout << mk_pp(tmp, m) << "\n";
+                      tout << "old fml: " << mk_pp(save_result, m) << "\n";
+                      tout << "new fml: " << mk_pp(result, m) << "\n";
                       );           
             }            
         }
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index 4799b8b9f..9ad787c2a 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_macro_finder            = p.macro_finder();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
+    m_refine_inj_axiom        = p.refine_inj_axioms();
 }
 
 void preprocessor_params::updt_params(params_ref const & p) {
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 50bb6422b..869b8cdc4 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -14,6 +14,7 @@ def_module_params(module_name='smt',
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
+                          ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 7281a5daa..7287cac2f 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -22,6 +22,7 @@ Revision History:
 void theory_arith_params::updt_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_arith_random_initial_value = p.arith_random_initial_value();
+    m_arith_random_seed = p.random_seed();
     m_arith_mode = static_cast<arith_solver_id>(p.arith_solver());
     m_nl_arith = p.arith_nl();
     m_nl_arith_gb = p.arith_nl_gb();
diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp
index 5e66ab738..3b0ec8e5f 100644
--- a/src/smt/proto_model/datatype_factory.cpp
+++ b/src/smt/proto_model/datatype_factory.cpp
@@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     // Approach 2)
     // For recursive datatypes.
     // search for constructor...
+    unsigned num_iterations = 0;
     if (m_util.is_recursive(s)) {
         while(true) {
+            ++num_iterations;
             TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
             ptr_vector<func_decl>::const_iterator it   = constructors->begin();
@@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                           << found_sibling << "\n";);
                     if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
-                        expr * maybe_new_arg = get_almost_fresh_value(s_arg);
+                        expr * maybe_new_arg = 0;
+                        if (num_iterations <= 1) {
+                            maybe_new_arg = get_almost_fresh_value(s_arg);
+                        }
+                        else {
+                            maybe_new_arg = get_fresh_value(s_arg);
+                        }
                         if (!maybe_new_arg) {
                             TRACE("datatype_factory", 
                                   tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
@@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                 if (found_sibling) {
                     expr_ref new_value(m_manager);
                     new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
+                    TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
                     m_last_fresh_value.insert(s, new_value);
                     if (!set->contains(new_value)) {
                         register_value(new_value);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 02ee06985..4f3c73ce6 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3945,7 +3945,7 @@ namespace smt {
               m_fingerprints.display(tout); 
               );
         failure fl = get_last_search_failure();
-        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
+        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
             // don't generate model.
             return;
         }
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index cf22c3e3a..6c138fd57 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -102,6 +102,7 @@ namespace smt {
                     if (th && th->build_models()) {
                         if (r->get_th_var(th->get_id()) != null_theory_var) {
                             proc = th->mk_value(r, *this);
+                            SASSERT(proc);
                         }
                         else {
                             TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
@@ -110,6 +111,7 @@ namespace smt {
                     }
                     else {
                         proc = mk_model_value(r);
+                        SASSERT(proc);
                     }
                 }
                 SASSERT(proc);
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 04e16e778..368ccb87d 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -193,7 +193,7 @@ namespace smt {
             return true;
         }
 
-        if (!r.get_base_var() == x && x > y) {
+        if (r.get_base_var() != x && x > y) {
             std::swap(x, y);
             k.neg();
         }
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index a338be50a..8b3021573 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1198,6 +1198,7 @@ namespace smt {
     void theory_bv::relevant_eh(app * n) {
         ast_manager & m = get_manager();
         context & ctx   = get_context();
+        TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";);
         if (m.is_bool(n)) {
             bool_var v = ctx.get_bool_var(n);
             atom * a   = get_bv2a(v);
diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp
index 4ef1bd8e0..fc9138bf6 100644
--- a/src/smt/theory_dl.cpp
+++ b/src/smt/theory_dl.cpp
@@ -162,7 +162,7 @@ namespace smt {
             m.register_factory(alloc(dl_factory, m_util, m.get_model()));
         }
         
-        virtual smt::model_value_proc * mk_value(smt::enode * n) {
+        virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
             return alloc(dl_value_proc, *this, n);
         }
 
@@ -201,9 +201,8 @@ namespace smt {
             if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
                 SASSERT(!m_reps.contains(s));
                 sort* bv = b().mk_sort(64);
-                // TBD: filter these from model.
-                r = m().mk_fresh_func_decl("rep",1, &s,bv);
-                v = m().mk_fresh_func_decl("val",1, &bv,s);
+                r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
+                v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
                 m_reps.insert(s, r);
                 m_vals.insert(s, v);
                 add_trail(r);
diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp
index 872981283..00d2f53ad 100644
--- a/src/tactic/arith/bv2int_rewriter.cpp
+++ b/src/tactic/arith/bv2int_rewriter.cpp
@@ -218,6 +218,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
     if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
         align_sizes(s1, t1, false);
         result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
+        TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
         return BR_DONE;
     }
 
@@ -232,6 +233,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
         u1 = mk_bv_add(s1, u1, false);
         align_sizes(u1, t1, false);
         result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
+        TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";);
         return BR_DONE;
     }
     
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index d81b4fa13..1f560ef62 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -29,14 +29,15 @@ struct cofactor_elim_term_ite::imp {
     ast_manager &      m;
     params_ref         m_params;
     unsigned long long m_max_memory;
-    volatile bool m_cancel;
+    bool               m_cofactor_equalities;
+    volatile bool      m_cancel;
 
     void checkpoint() { 
         cooperate("cofactor ite");
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         if (m_cancel)
-            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            throw tactic_exception(TACTIC_CANCELED_MSG);
     }
 
     // Collect atoms that contain term if-then-else
@@ -111,7 +112,7 @@ struct cofactor_elim_term_ite::imp {
                 frame & fr    = m_frame_stack.back();
                 expr * t      = fr.m_t;
                 bool form_ctx = fr.m_form_ctx;
-                TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                TRACE("cofactor", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
 
                 m_owner.checkpoint();
                 
@@ -150,7 +151,7 @@ struct cofactor_elim_term_ite::imp {
                     }
                     if (i < num_args) {
                         m_has_term_ite.mark(t);
-                        TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                        TRACE("cofactor", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
                         save_candidate(t, form_ctx);
                     }
                 }
@@ -167,6 +168,7 @@ struct cofactor_elim_term_ite::imp {
     };
 
     expr * get_first(expr * t) { 
+        TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
         typedef std::pair<expr *, unsigned> frame;
         expr_fast_mark1         visited;            
         sbuffer<frame>          stack;    
@@ -225,6 +227,7 @@ struct cofactor_elim_term_ite::imp {
        \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
     */
     expr * get_best(expr * t) {
+        TRACE("cofactor", tout << mk_ismt2_pp(t, m) << "\n";);
         typedef std::pair<expr *, unsigned> frame;
         obj_map<expr, unsigned> occs;
         expr_fast_mark1         visited;            
@@ -299,12 +302,17 @@ struct cofactor_elim_term_ite::imp {
             }
         }
         visited.reset();
-        CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
+        CTRACE("cofactor", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
         return best;
     }
 
     void updt_params(params_ref const & p) {
         m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+        m_cofactor_equalities = p.get_bool("cofactor_equalities", true);
+    }
+
+    void collect_param_descrs(param_descrs & r) {
+        r.insert("cofactor_equalities", CPK_BOOL, "(default: true) use equalities to rewrite bodies of ite-expressions. This is potentially expensive.");
     }
 
     void set_cancel(bool f) {
@@ -354,16 +362,16 @@ struct cofactor_elim_term_ite::imp {
                 m_term = 0;
                 expr * lhs;
                 expr * rhs;
-                if (m.is_eq(t, lhs, rhs)) {
+                if (m_owner.m_cofactor_equalities && m.is_eq(t, lhs, rhs)) {
                     if (m.is_unique_value(lhs)) {
                         m_term  = rhs;
                         m_value = to_app(lhs); 
-                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                        TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
                     }
                     else if (m.is_unique_value(rhs)) {
                         m_term  = lhs;
                         m_value = to_app(rhs);
-                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                        TRACE("cofactor", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
                     }
                 }
                 // TODO: bounds
@@ -467,7 +475,7 @@ struct cofactor_elim_term_ite::imp {
                     m_cofactor.set_cofactor_atom(neg_c);
                     m_cofactor(curr, neg_cofactor);
                     curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                    TRACE("cofactor", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
                 }
             }
             return false;
@@ -522,7 +530,7 @@ struct cofactor_elim_term_ite::imp {
         
         void cofactor(expr * t, expr_ref & r) {
             unsigned step = 0;
-            TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
+            TRACE("cofactor", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
             expr_ref curr(m);
             curr = t;
             while (true) {
@@ -543,21 +551,20 @@ struct cofactor_elim_term_ite::imp {
                 m_cofactor(curr, neg_cofactor);
                 if (pos_cofactor == neg_cofactor) {
                     curr = pos_cofactor;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
+                else if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
                     curr = c;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
+                else if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
                     curr = neg_c;
-                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
-                    continue;
                 }
-                curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
-                TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                else {
+                    curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
+                }
+                TRACE("cofactor", 
+                      tout << "cofactor_ite step: " << step << "\n";
+                      tout << "cofactor: " << mk_ismt2_pp(c, m) << "\n";
+                      tout << mk_ismt2_pp(curr, m) << "\n";);
             }
         }
 
@@ -570,6 +577,7 @@ struct cofactor_elim_term_ite::imp {
         
         void operator()(expr * t, expr_ref & r) {
             ptr_vector<expr> new_args;
+            SASSERT(m_frames.empty());
             m_frames.push_back(frame(t, true));
             while (!m_frames.empty()) {
                 m_owner.checkpoint();
@@ -649,7 +657,8 @@ struct cofactor_elim_term_ite::imp {
 
     imp(ast_manager & _m, params_ref const & p):
         m(_m),
-        m_params(p) {
+        m_params(p),
+        m_cofactor_equalities(true) {
         m_cancel = false;
         updt_params(p);
     }
@@ -686,7 +695,8 @@ void cofactor_elim_term_ite::updt_params(params_ref const & p) {
     m_imp->updt_params(p);
 }
 
-void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) {
+void cofactor_elim_term_ite::collect_param_descrs(param_descrs & r) {
+    m_imp->collect_param_descrs(r);
 }
 
 void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h
index 9b325b1f0..ce2f31ea0 100644
--- a/src/tactic/core/cofactor_elim_term_ite.h
+++ b/src/tactic/core/cofactor_elim_term_ite.h
@@ -31,7 +31,7 @@ public:
     virtual ~cofactor_elim_term_ite();
 
     void updt_params(params_ref const & p);
-    static void get_param_descrs(param_descrs & r);
+    void collect_param_descrs(param_descrs & r);
 
     void operator()(expr * t, expr_ref & r);
     
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index 16b4d1ad4..bc719a85e 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -52,8 +52,7 @@ public:
 
     virtual ~cofactor_term_ite_tactic() {}
     virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
-    static  void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); }
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
+    virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); }
     
     virtual void operator()(goal_ref const & g, 
                             goal_ref_buffer & result, 
diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp
index da4c71e54..ba6ee4f0d 100644
--- a/src/tactic/filter_model_converter.cpp
+++ b/src/tactic/filter_model_converter.cpp
@@ -43,6 +43,7 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
         if (fs.is_marked(f))
             continue;
         func_interp * fi = old_model->get_func_interp(f);
+        SASSERT(fi);
         new_model->register_decl(f, fi->copy());
     }
     new_model->copy_usort_interps(*old_model);
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 603898af8..8ff5f8e8f 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -165,6 +165,14 @@ public:
         SASSERT(e);
         return e->get_data().m_value;
     }
+
+    value const & operator[](key * k) const {
+        return find(k);
+    }
+
+    value & operator[](key * k) {
+        return find(k);
+    }
     
     iterator find_iterator(Key * k) const { 
         return m_table.find(key_data(k));

From ab13987884de98e21184550b5a2ea95be0544a8f Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 11:16:24 -0700
Subject: [PATCH 06/42] working on python interp

---
 src/api/api_interp.cpp    | 80 +++++++++++++++++++++++++++++++
 src/api/python/z3.py      | 15 ++++++
 src/api/python/z3types.py |  3 ++
 src/api/z3_api.h          | 99 +++++++++++++++++++++++++++++++++++++++
 src/interp/iz3interp.cpp  |  3 ++
 src/interp/iz3interp.h    |  2 +
 6 files changed, 202 insertions(+)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 2c88a1978..4ea0f5d77 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -38,6 +38,7 @@ Revision History:
 #include"iz3hash.h"
 #include"iz3pp.h"
 #include"iz3checker.h"
+#include"scoped_proof.h"
 
 using namespace stl_ext;
 
@@ -290,6 +291,85 @@ extern "C" {
     opts->map[name] = value;
   }
 
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
+    Z3_TRY;
+    LOG_Z3_get_interpolant(c, pf, pat, p);
+    RESET_ERROR_CODE();
+
+    Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+    mk_c(c)->save_object(v);
+
+    ast *_pf = to_ast(pf);
+    ast *_pat = to_ast(pat);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    iz3interpolate(_m,
+		   _pf,
+		   cnsts,
+		   _pat,
+		   interp,
+		   (interpolation_options_struct *) 0 // ignore params for now
+		   );
+    
+    // copy result back
+    for(unsigned i = 0; i < interp.size(); i++){
+      v->m_ast_vector.push_back(interp[i]);
+      _m.dec_ref(interp[i]);
+    }
+    RETURN_Z3(of_ast_vector(v));
+    Z3_CATCH_RETURN(0);
+  }
+
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp){
+    Z3_TRY;
+    LOG_Z3_compute_interpolant(c, pat, p, out_interp);
+    RESET_ERROR_CODE();
+
+
+    params_ref &_p = to_params(p)->m_params;
+    scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
+    scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
+    m_solver.get()->updt_params(_p); // why do we have to do this?
+    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
+
+    ast *_pat = to_ast(pat);
+    
+    ptr_vector<ast> interp;
+    ptr_vector<ast> cnsts; // to throw away
+    
+    ast_manager &_m = mk_c(c)->m();
+
+    model_ref m;
+    lbool _status = iz3interpolate(_m,
+				   *(m_solver.get()),
+				   _pat,
+				   cnsts,
+				   interp,
+				   m,
+				   0 // ignore params for now
+				   );
+    
+    Z3_lbool status = of_lbool(_status);
+    
+    Z3_ast_vector_ref *v = 0;
+    if(_status == l_false){
+      // copy result back
+      v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+      mk_c(c)->save_object(v);
+      for(unsigned i = 0; i < interp.size(); i++){
+	v->m_ast_vector.push_back(interp[i]);
+	_m.dec_ref(interp[i]);
+      }
+    }
+    *out_interp = of_ast_vector(v);
+    
+    return status;
+    Z3_CATCH_RETURN(Z3_L_UNDEF);
+  }
 
 
 };
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index ce53a4c1f..533a71956 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7253,3 +7253,18 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
+def Interp(a):
+     ctx = main_ctx()
+     s = BoolSort(ctx)
+     a = s.cast(a)
+     return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+
+def tree_interpolant(f,p=None,ctx=None):
+    ctx = _get_ctx(ctx)
+    ptr = (ctypes.POINTER(AstVectorObj) * 1)()
+    if p == None:
+        p = ParamsRef(ctx)
+    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr[0])
+    if res == Z3_L_FALSE:
+        return AstVector(ptr[0],ctx)
+    raise NoInterpolant()
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index a26a958c0..56316eb46 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -109,3 +109,6 @@ class FuncEntryObj(ctypes.c_void_p):
 class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
+
+class NoInterpolant():
+    def __init__(self):
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 94e20eceb..554c792e3 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7699,6 +7699,105 @@ END_MLAPI_EXCLUDE
 
   Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
 
+  /** Compute an interpolant from a refutation. This takes a proof of
+      "false" from a set of formulas C, and an interpolation
+      pattern. The pattern pat is a formula combining the formulas in C
+      using logical conjunction and the "interp" operator (see
+      #Z3_mk_interp). This interp operator is logically the identity
+      operator. It marks the sub-formulas of the pattern for which interpolants should
+      be computed. The interpolant is a map sigma from marked subformulas to
+      formulas, such that, for each marked subformula phi of pat (where phi sigma
+      is phi with sigma(psi) substituted for each subformula psi of phi such that
+      psi in dom(sigma)):
+
+      1) phi sigma implies sigma(phi), and
+
+      2) sigma(phi) is in the common uninterpreted vocabulary between
+      the formulas of C occurring in phi and those not occurring in
+      phi
+
+      and moreover pat sigma implies false. In the simplest case
+      an interpolant for the pattern "(and (interp A) B)" maps A
+      to an interpolant for A /\ B. 
+
+      The return value is a vector of formulas representing sigma. The
+      vector contains sigma(phi) for each marked subformula of pat, in
+      pre-order traversal. This means that subformulas of phi occur before phi
+      in the vector. Also, subformulas that occur multiply in pat will
+      occur multiply in the result vector.
+
+      In particular, calling Z3_get_interpolant on a pattern of the
+      form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
+      result in a sequence interpolant for A_1, A_2,... A_N. 
+
+      Neglecting interp markers, the pattern must be a conjunction of
+      formulas in C, the set of premises of the proof. Otherwise an
+      error is flagged.
+
+      Any premises of the proof not present in the pattern are
+      treated as "background theory". Predicate and function symbols
+      occurring in the background theory are treated as interpreted and
+      thus always allowed in the interpolant.
+
+      Interpolant may not necessarily be computable from all
+      proofs. To be sure an interpolant can be computed, the proof
+      must be generated by an SMT solver for which interpoaltion is
+      supported, and the premises must be expressed using only
+      theories and operators for which interpolation is supported.
+
+      Currently, the only SMT solver that is supported is the legacy
+      SMT solver. Such a solver is available as the default solver in
+      #Z3_context objects produced by #Z3_mk_interpolation_context.
+      Currently, the theories supported are equality with
+      uninterpreted functions, linear integer arithmetic, and the
+      theory of arrays (in SMT-LIB terms, this is AUFLIA).
+      Quantifiers are allowed. Use of any other operators (including
+      "labels") may result in failure to compute an interpolant from a
+      proof.
+
+      Parameters:
+
+      \param c logical context.
+      \param pf a refutation from premises (assertions) C
+      \param pat an interpolation pattern over C
+      \param p parameters
+
+       def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
+    */
+
+  Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
+
+  /* Compute an interpolant for an unsatisfiable conjunction of formulas.
+
+     This takes as an argument an interpolation pattern as in
+     #Z3_get_interpolant. This is a conjunction, some subformulas of
+     which are marked with the "interp" operator (see #Z3_mk_interp).
+     
+     The conjunction is first checked for unsatisfiability. The result
+     of this check is returned in the out parameter "status". If the result
+     is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
+     and returned as a vector of formulas. Otherwise the return value is
+     an empty formula. 
+
+     See #Z3_get_interpolant for a discussion of supported theories.
+
+     The advantage of this function over #Z3_get_interpolant is that
+     it is not necessary to create a suitable SMT solver and generate
+     a proof. The disadvantage is that it is not possible to use the
+     solver incrementally.
+
+     Parameters:
+     
+     \param c logical context.
+     \param pat an interpolation pattern
+     \param p parameters
+     \param status returns the status of the sat check
+     
+     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR)))
+  */
+  
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp);
+
 
 /** Constant reprepresenting a root of a formula tree for tree interpolation */
 #define IZ3_ROOT SHRT_MAX
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 1ae3e3a1b..0d394090f 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -41,6 +41,7 @@ Revision History:
 #include "iz3hash.h"
 #include "iz3interp.h"
 
+#include"scoped_proof.h"
 
 
 using namespace stl_ext;
@@ -503,6 +504,8 @@ lbool iz3interpolate(ast_manager &_m_manager,
   return res;
 }
 
+
+
 void interpolation_options_struct::apply(iz3base &b){
   for(stl_ext::hash_map<std::string,std::string>::iterator it = map.begin(), en = map.end();
       it != en;
diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h
index 52aa716c3..1c6f9513e 100644
--- a/src/interp/iz3interp.h
+++ b/src/interp/iz3interp.h
@@ -76,6 +76,7 @@ void iz3interpolate(ast_manager &_m_manager,
 		    ptr_vector<ast> &interps,
 		    interpolation_options_struct * options);
 
+
 /* Compute an interpolant from an ast representing an interpolation
    problem, if unsat, else return a model (if enabled). Uses the
    given solver to produce the proof/model. Also returns a vector
@@ -90,4 +91,5 @@ lbool iz3interpolate(ast_manager &_m_manager,
 		     model_ref &m,
 		     interpolation_options_struct * options);
 
+
 #endif

From 5a107095c937dd879ae411cfce87dc8806c5eba3 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 11:32:51 -0700
Subject: [PATCH 07/42] removing python changes for interp

---
 src/api/python/z3.py      | 15 ---------------
 src/api/python/z3types.py |  2 --
 2 files changed, 17 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 533a71956..ce53a4c1f 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7253,18 +7253,3 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
-def Interp(a):
-     ctx = main_ctx()
-     s = BoolSort(ctx)
-     a = s.cast(a)
-     return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
-
-def tree_interpolant(f,p=None,ctx=None):
-    ctx = _get_ctx(ctx)
-    ptr = (ctypes.POINTER(AstVectorObj) * 1)()
-    if p == None:
-        p = ParamsRef(ctx)
-    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr[0])
-    if res == Z3_L_FALSE:
-        return AstVector(ptr[0],ctx)
-    raise NoInterpolant()
diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py
index 56316eb46..593312d68 100644
--- a/src/api/python/z3types.py
+++ b/src/api/python/z3types.py
@@ -110,5 +110,3 @@ class RCFNumObj(ctypes.c_void_p):
   def __init__(self, e): self._as_parameter_ = e
   def from_param(obj): return obj
 
-class NoInterpolant():
-    def __init__(self):

From 6880945435696f9090a99fd241cdc7adcc467cf1 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 15:30:24 -0700
Subject: [PATCH 08/42] added simple interpolation bindings for python

---
 src/api/api_interp.cpp |  22 ++++++--
 src/api/python/z3.py   | 125 +++++++++++++++++++++++++++++++++++++++++
 src/api/z3_api.h       |   9 ++-
 3 files changed, 149 insertions(+), 7 deletions(-)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 4ea0f5d77..03d5ff843 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -324,17 +324,20 @@ extern "C" {
     Z3_CATCH_RETURN(0);
   }
 
-  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp){
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
     Z3_TRY;
-    LOG_Z3_compute_interpolant(c, pat, p, out_interp);
+    LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
     RESET_ERROR_CODE();
 
 
-    params_ref &_p = to_params(p)->m_params;
+    // params_ref &_p = to_params(p)->m_params;
+    params_ref _p;
+    _p.set_bool("proof", true); // this is currently useless
+
+    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
     scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
     scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
     m_solver.get()->updt_params(_p); // why do we have to do this?
-    scoped_proof_mode spm(mk_c(c)->m(),PGM_FINE);
 
     ast *_pat = to_ast(pat);
     
@@ -356,6 +359,8 @@ extern "C" {
     Z3_lbool status = of_lbool(_status);
     
     Z3_ast_vector_ref *v = 0;
+    *model = 0;
+
     if(_status == l_false){
       // copy result back
       v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
@@ -365,6 +370,15 @@ extern "C" {
 	_m.dec_ref(interp[i]);
       }
     }
+    else {
+      model_ref _m;
+      m_solver.get()->get_model(_m);
+      Z3_model_ref *crap = alloc(Z3_model_ref);
+      crap->m_model = _m.get();
+      mk_c(c)->save_object(crap);
+      *model = of_model(crap);
+    }
+
     *out_interp = of_ast_vector(v);
     
     return status;
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index ce53a4c1f..9c5ff8f14 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7253,3 +7253,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
     dsz, dnames, ddecls = _dict2darray(decls, ctx)
     return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
    
+def Interp(a,ctx=None):
+    """Create an interpolation operator.
+    
+    The argument is an interpolation pattern (see tree_interpolant). 
+
+    >>> x = Int('x')
+    >>> print Interp(x>0)
+    interp(x > 0)
+    """
+    ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
+    s = BoolSort(ctx)
+    a = s.cast(a)
+    return BoolRef(Z3_mk_interp(ctx.ref(), a.as_ast()), ctx)
+
+def tree_interpolant(pat,p=None,ctx=None):
+    """Compute interpolant for a tree of formulas.
+
+    The input is an interpolation pattern over a set of formulas C.
+    The pattern pat is a formula combining the formulas in C using
+    logical conjunction and the "interp" operator (see Interp). This
+    interp operator is logically the identity operator. It marks the
+    sub-formulas of the pattern for which interpolants should be
+    computed. The interpolant is a map sigma from marked subformulas
+    to formulas, such that, for each marked subformula phi of pat
+    (where phi sigma is phi with sigma(psi) substituted for each
+    subformula psi of phi such that psi in dom(sigma)):
+
+      1) phi sigma implies sigma(phi), and
+
+      2) sigma(phi) is in the common uninterpreted vocabulary between
+      the formulas of C occurring in phi and those not occurring in
+      phi
+
+      and moreover pat sigma implies false. In the simplest case
+      an interpolant for the pattern "(and (interp A) B)" maps A
+      to an interpolant for A /\ B. 
+
+      The return value is a vector of formulas representing sigma. This
+      vector contains sigma(phi) for each marked subformula of pat, in
+      pre-order traversal. This means that subformulas of phi occur before phi
+      in the vector. Also, subformulas that occur multiply in pat will
+      occur multiply in the result vector.
+
+    If pat is satisfiable, raises an object of class ModelRef
+    that represents a model of pat.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
+    [Not(x >= 0), Not(y <= 2)]
+    """
+    f = pat
+    ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
+    ptr = (AstVectorObj * 1)()
+    mptr = (Model * 1)()
+    if p == None:
+        p = ParamsRef(ctx)
+    res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
+    if res == Z3_L_FALSE:
+        return AstVector(ptr[0],ctx)
+    raise ModelRef(mptr[0], ctx)
+
+def binary_interpolant(a,b,p=None,ctx=None):
+    """Compute an interpolant for a binary conjunction.
+
+    If a & b is unsatisfiable, returns an interpolant for a & b.
+    This is a formula phi such that
+
+    1) a implies phi
+    2) b implies not phi
+    3) All the uninterpreted symbols of phi occur in both a and b.
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a &b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> print binary_interpolant(x<0,x>2)
+    x <= 2
+    """
+    f = And(Interp(a),b)
+    return tree_interpolant(f,p,ctx)[0]
+
+def sequence_interpolant(v,p=None,ctx=None):
+    """Compute interpolant for a sequence of formulas.
+
+    If len(v) == N, and if the conjunction of the formulas in v is
+    unsatisfiable, the interpolant is a sequence of formulas w
+    such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
+
+    1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
+    2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
+    and v[i+1]..v[n]
+    
+    Requires len(v) >= 1. 
+
+    If a & b is satisfiable, raises an object of class ModelRef
+    that represents a model of a & b.
+
+    If parameters p are supplied, these are used in creating the
+    solver that determines satisfiability.
+
+    >>> x = Int('x')
+    >>> y = Int('y')
+    >>> print sequence_interpolant([x < 0, y == x , y > 2])
+    [Not(x >= 0), Not(y >= 0)]
+
+    >>> g = And(Interp(x<0),x<2)
+    >>> try:
+    ...     print tree_interpolant(g).sexpr()
+    ... except ModelRef as m:
+    ...     print m.sexpr()
+    (define-fun x () Int
+      (- 1))
+    """
+    f = v[0]
+    for i in range(1,len(v)):
+        f = And(Interp(f),v[i])
+    return tree_interpolant(f,p,ctx)
+
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 554c792e3..b9f4975e8 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7790,13 +7790,16 @@ END_MLAPI_EXCLUDE
      
      \param c logical context.
      \param pat an interpolation pattern
-     \param p parameters
+     \param p parameters for solver creation
      \param status returns the status of the sat check
+     \param model returns model if satisfiable
+
+     Return value: status of SAT check
      
-     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR)))
+     def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
   */
   
-  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp);
+  Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *interp, __out Z3_model *model);
 
 
 /** Constant reprepresenting a root of a formula tree for tree interpolation */

From e17af8a5dec251082c2843223b9ffdaca4d0ccf6 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 6 Aug 2014 15:34:58 -0700
Subject: [PATCH 09/42] doc fix for interpolation bindings for python

---
 src/api/python/z3.py | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 9c5ff8f14..50d29a790 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7306,6 +7306,14 @@ def tree_interpolant(pat,p=None,ctx=None):
     >>> y = Int('y')
     >>> print tree_interpolant(And(Interp(x < 0), Interp(y > 2), x == y))
     [Not(x >= 0), Not(y <= 2)]
+
+    >>> g = And(Interp(x<0),x<2)
+    >>> try:
+    ...     print tree_interpolant(g).sexpr()
+    ... except ModelRef as m:
+    ...     print m.sexpr()
+    (define-fun x () Int
+      (- 1))
     """
     f = pat
     ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
@@ -7364,14 +7372,6 @@ def sequence_interpolant(v,p=None,ctx=None):
     >>> y = Int('y')
     >>> print sequence_interpolant([x < 0, y == x , y > 2])
     [Not(x >= 0), Not(y >= 0)]
-
-    >>> g = And(Interp(x<0),x<2)
-    >>> try:
-    ...     print tree_interpolant(g).sexpr()
-    ... except ModelRef as m:
-    ...     print m.sexpr()
-    (define-fun x () Int
-      (- 1))
     """
     f = v[0]
     for i in range(1,len(v)):

From 3d995648eea72722cee40bd51694c2b2a2d3f374 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 7 Aug 2014 20:39:20 +0900
Subject: [PATCH 10/42] partial fix to model generation bug for non-linear
 constraints: avoid epsilon refinment for non-shared variables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith.h      |  1 +
 src/smt/theory_arith_core.h |  3 ++-
 src/smt/theory_arith_nl.h   | 12 ++++++++----
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index e7037f31a..998dd72e6 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -85,6 +85,7 @@ namespace smt {
         typedef typename Ext::numeral     numeral;
         typedef typename Ext::inf_numeral inf_numeral;
         typedef vector<numeral> numeral_vector; 
+        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
 
         static const int    dead_row_id = -1;
     protected:
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 195d78e25..fbc043048 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2780,7 +2780,6 @@ namespace smt {
     */
     template<typename Ext>
     void theory_arith<Ext>::refine_epsilon() {
-        typedef map<rational, theory_var, obj_hash<rational>, default_eq<rational> > rational2var;
         while (true) {
             rational2var mapping;
             theory_var num = get_num_vars();
@@ -2788,6 +2787,8 @@ namespace smt {
             for (theory_var v = 0; v < num; v++) {
                 if (is_int(v))
                     continue;
+                if (!get_context().is_shared(get_enode(v)))
+                    continue;
                 inf_numeral const & val = get_value(v);
                 rational value = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
                 theory_var v2;
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index bab921ed2..d02c9e540 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -654,6 +654,7 @@ namespace smt {
         }
         return get_value(v, computed_epsilon) == val;
     }
+    
 
     /**
        \brief Return true if for every monomial x_1 * ... * x_n,
@@ -2309,8 +2310,9 @@ namespace smt {
         if (m_nl_monomials.empty())
             return FC_DONE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return FC_DONE;
+        }
 
         if (!m_params.m_nl_arith)
             return FC_GIVEUP;
@@ -2338,9 +2340,10 @@ namespace smt {
         if (!max_min_nl_vars())
             return FC_CONTINUE;
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
-        
+        }
+
         svector<theory_var> vars;
         get_non_linear_cluster(vars);
 
@@ -2391,8 +2394,9 @@ namespace smt {
         }
         while (m_nl_strategy_idx != old_idx);
 
-        if (check_monomial_assignments())
+        if (check_monomial_assignments()) {
             return m_liberal_final_check || !m_changed_assignment ? FC_DONE : FC_CONTINUE;
+        }
 
         TRACE("non_linear", display(tout););
 

From 0df0174d6216a9cbaeb1dab0443e9a626ec5dddb Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 8 Aug 2014 15:24:08 +0100
Subject: [PATCH 11/42] .NET API: Enabled .xml documentation generation by
 default.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/mk_util.py | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index b73f7a7a8..035cdd3c4 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1151,7 +1151,11 @@ class DotNetDLLComponent(Component):
                 out.write(' ')
                 out.write(cs_file)
             out.write('\n')
-            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /define:DEBUG;TRACE /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /debug+ /debug:full /filealign:512 /optimize- /linkresource:%s.dll /out:%s.dll /target:library' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name))
+            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name))
+            if DEBUG_MODE:
+                out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-')
+            else:
+                out.write(' /optimize+')
             if VS_X64:
                 out.write(' /platform:x64')
             else:
@@ -1174,6 +1178,13 @@ class DotNetDLLComponent(Component):
             mk_dir(os.path.join(dist_path, 'bin'))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
                         '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+            shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
+                        '%s.xml' % os.path.join(dist_path, 'bin', self.dll_name))
+            if DEBUG_MODE:
+                shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
+                            '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
+
+
 
     def mk_unix_dist(self, build_path, dist_path):
         # Do nothing

From 47ac5c06333bdd81b1f8084c4e5416cc5f235d23 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 9 Aug 2014 11:41:04 +0900
Subject: [PATCH 12/42] fix doc bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/Context.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 41ac1fa31..16073f3b3 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3523,7 +3523,7 @@ namespace Microsoft.Z3
         /// </summary>
         /// <remarks>
         /// The list of all configuration parameters can be obtained using the Z3 executable:
-        /// <c>z3.exe -ini?</c>
+        /// <c>z3.exe -p</c>
         /// Only a few configuration parameters are mutable once the context is created.
         /// An exception is thrown when trying to modify an immutable parameter.
         /// </remarks>

From 5a45711f22d92880c771e81e95da0c6525c781a4 Mon Sep 17 00:00:00 2001
From: mattpark <mattpark@microsoft.com>
Date: Mon, 11 Aug 2014 15:44:10 +0100
Subject: [PATCH 13/42] Dealt with some concurrency issues due to concurrent
 GC.

---
 src/api/dotnet/Context.cs  | 2 +-
 src/api/dotnet/Z3Object.cs | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 16073f3b3..5436fe0a0 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal uint refCount = 0;
+        internal int refCount = 0;
 
         /// <summary>
         /// Finalizer.
diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs
index e8654ce21..8e474041a 100644
--- a/src/api/dotnet/Z3Object.cs
+++ b/src/api/dotnet/Z3Object.cs
@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Threading;
 
 namespace Microsoft.Z3
 {
@@ -50,8 +51,7 @@ namespace Microsoft.Z3
 
             if (m_ctx != null)
             {
-                m_ctx.refCount--;
-                if (m_ctx.refCount == 0)
+                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
                     GC.ReRegisterForFinalize(m_ctx);
                 m_ctx = null;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
@@ -85,7 +85,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
             IncRef(obj);
             m_n_obj = obj;

From 0cf1f9c2106ee7110465809f0fd000946c9d0e9a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 14 Aug 2014 12:15:58 +0100
Subject: [PATCH 14/42] .NET API context refcounting; changed int to long to be
 on the safe side on 64-bit platforms.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/dotnet/Context.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 5436fe0a0..2b88cbab7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal int refCount = 0;
+        internal long refCount = 0;
 
         /// <summary>
         /// Finalizer.

From 37ed4b04d078d6d1e35db2799d769e8d4b87f775 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 14 Aug 2014 12:18:00 +0100
Subject: [PATCH 15/42] Bugfix: param_refs didn't make it through to
 smt::solver (smt_params) in some cases.

Thanks to user xor88 for pointing us in the right direction!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/api_solver.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index ac30a0c21..c8b1723f1 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -40,6 +40,7 @@ extern "C" {
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
+        s->m_solver->updt_params(p);
     }
 
     static void init_solver(Z3_context c, Z3_solver s) {

From 60054ce469c3e2bc8c34e7b9285c8450e4232812 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Aug 2014 21:20:56 -0700
Subject: [PATCH 16/42] fix cache bug in PDR reported by Phillip Ruemmer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp | 38 +++++++++++++++++++++++++------------
 src/muz/pdr/pdr_context.h   | 13 ++++++++-----
 2 files changed, 34 insertions(+), 17 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index b09280d35..94dd5d0a0 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -736,6 +736,11 @@ namespace pdr {
         m_closed = true; 
     }
 
+    void model_node::reopen() {
+        SASSERT(m_closed);
+        m_closed = false;
+    }
+
     static bool is_ini(datalog::rule const& r) {
         return r.get_uninterpreted_tail_size() == 0;
     }
@@ -745,6 +750,7 @@ namespace pdr {
             return const_cast<datalog::rule*>(m_rule);
         }
         // only initial states are not set by the PDR search.
+        SASSERT(m_model.get());
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -864,9 +870,10 @@ namespace pdr {
     }
 
     void model_search::add_leaf(model_node& n) {
-        unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
-        ++count;
-        if (count == 1 || is_repeated(n)) {
+        model_nodes ns;
+        model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
+        nodes.push_back(&n);
+        if (nodes.size() == 1 || is_repeated(n)) {
             set_leaf(n);
         }
         else {
@@ -875,7 +882,7 @@ namespace pdr {
     }
 
     void model_search::set_leaf(model_node& n) {
-        erase_children(n);
+        erase_children(n, true);
         SASSERT(n.is_open());      
         enqueue_leaf(n);
     }
@@ -897,7 +904,7 @@ namespace pdr {
         set_leaf(*root);
     }
 
-    obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
+    obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
         unsigned l = n.orig_level();
         if (l >= m_cache.size()) {
             m_cache.resize(l + 1);
@@ -905,7 +912,7 @@ namespace pdr {
         return m_cache[l];
     }
 
-    void model_search::erase_children(model_node& n) {
+    void model_search::erase_children(model_node& n, bool backtrack) {
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
         erase_leaf(n);
@@ -916,13 +923,20 @@ namespace pdr {
             nodes.push_back(m);
             todo.append(m->children());
             erase_leaf(*m);
-            remove_node(*m);
+            remove_node(*m, backtrack);
         }
         std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
     }
 
-    void model_search::remove_node(model_node& n) {
-        if (0 == --cache(n).find(n.state())) {
+    void model_search::remove_node(model_node& n, bool backtrack) {
+        model_nodes& nodes = cache(n).find(n.state());
+        nodes.erase(&n);
+        if (nodes.size() > 0 && n.is_open() && backtrack) {
+            for (unsigned i = 0; i < nodes.size(); ++i) {
+                nodes[i]->reopen();
+            }
+        }
+        if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
     }
@@ -1203,8 +1217,8 @@ namespace pdr {
 
     void model_search::reset() {
         if (m_root) {
-            erase_children(*m_root);
-            remove_node(*m_root);
+            erase_children(*m_root, false);
+            remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
         }
@@ -1240,7 +1254,7 @@ namespace pdr {
           m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
-          m_search(m_params.bfs_model_search()),
+          m_search(m_params.bfs_model_search(), m),
           m_last_result(l_undef),
           m_inductive_lvl(0),
           m_expanded_lvl(0),
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 8a4f3e438..a85011600 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -231,6 +231,7 @@ namespace pdr {
         }
 
         void set_closed();     
+        void reopen();
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
@@ -243,19 +244,21 @@ namespace pdr {
     };
 
     class model_search {
+        typedef ptr_vector<model_node> model_nodes;
+        ast_manager&       m;
         bool               m_bfs;
         model_node*        m_root;
         std::deque<model_node*> m_leaves;
-        vector<obj_map<expr, unsigned> > m_cache;
+        vector<obj_map<expr, model_nodes > > m_cache;
         
-        obj_map<expr, unsigned>& cache(model_node const& n);
-        void erase_children(model_node& n);
+        obj_map<expr, model_nodes>& cache(model_node const& n);
+        void erase_children(model_node& n, bool backtrack);
         void erase_leaf(model_node& n);
-        void remove_node(model_node& n);
+        void remove_node(model_node& n, bool backtrack);
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
         void update_models();
     public:
-        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
         ~model_search();
 
         void reset();

From 70a1155d711e38895174ada51d6568ae3af3b7ce Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 18 Aug 2014 17:13:16 -0700
Subject: [PATCH 17/42] fixed duality bug and added some code for returning
 bounded status (not yet used)

---
 src/duality/duality.h                    |  7 +++
 src/duality/duality_solver.cpp           | 24 +++++++++++
 src/muz/base/dl_context.h                |  3 ++
 src/muz/duality/duality_dl_interface.cpp | 55 +++++++++++++++++++++++-
 src/muz/fp/dl_cmds.cpp                   |  5 +++
 5 files changed, 93 insertions(+), 1 deletion(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index c315c5431..c1c9797f3 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1152,6 +1152,13 @@ protected:
 
       virtual void LearnFrom(Solver *old_solver) = 0;
 
+      /** Return true if the solution be incorrect due to recursion bounding.
+	  That is, the returned "solution" might contain all derivable facts up to the
+	  given recursion bound, but not be actually a fixed point.
+       */
+
+      virtual bool IsResultRecursionBounded() = 0;
+
       virtual ~Solver(){}
 
       static Solver *Create(const std::string &solver_class, RPFP *rpfp);
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 59611c814..681582415 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -768,6 +768,29 @@ namespace Duality {
       annot.Simplify();
     }    
 
+    bool recursionBounded;
+
+    /** See if the solution might be bounded. */
+    void TestRecursionBounded(){
+      recursionBounded = false;
+      if(RecursionBound == -1)
+	return;
+      for(unsigned i = 0; i < nodes.size(); i++){
+	Node *node = nodes[i];
+	std::vector<Node *> &insts = insts_of_node[node];
+	for(unsigned j = 0; j < insts.size(); j++)
+	  if(indset->Contains(insts[j]))
+	    if(NodePastRecursionBound(insts[j])){
+	      recursionBounded = true;
+	      return;
+	    }
+      }
+    }    
+
+    bool IsResultRecursionBounded(){
+      return recursionBounded;
+    }
+
     /** Generate a proposed solution of the input RPFP from
 	the unwinding, by unioning the instances of each node. */
     void GenSolutionFromIndSet(bool with_markers = false){
@@ -1026,6 +1049,7 @@ namespace Duality {
 	timer_stop("ProduceCandidatesForExtension");
 	if(candidates.empty()){
 	  GenSolutionFromIndSet();
+	  TestRecursionBounded();
 	  return true;
 	}
 	Candidate cand = candidates.front();
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 1952cc42f..7349fa889 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -53,6 +53,7 @@ namespace datalog {
         MEMOUT,
         INPUT_ERROR,
         APPROX,
+	BOUNDED,
         CANCELED
     };
 
@@ -304,6 +305,8 @@ namespace datalog {
            \brief Retrieve predicates
         */
         func_decl_set const& get_predicates() const { return m_preds; }
+	ast_ref_vector const &get_pinned() const {return m_pinned; }
+
         bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); }
         bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); }
 
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 0584e6b58..849cf94ea 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -36,6 +36,7 @@ Revision History:
 #include "model_v2_pp.h"
 #include "fixedpoint_params.hpp"
 #include "used_vars.h"
+#include "func_decl_dependencies.h"
 
 // template class symbol_table<family_id>;
 
@@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) {
     _d->rpfp->AssertAxiom(e);
   }
   
+  // make sure each predicate is the head of at least one clause
+  func_decl_set heads;
+  for(unsigned i = 0; i < clauses.size(); i++){
+    expr cl = clauses[i];
+
+    while(true){
+      if(cl.is_app()){
+	decl_kind k = cl.decl().get_decl_kind();
+	if(k == Implies)
+	  cl = cl.arg(1);
+	else {
+	  heads.insert(cl.decl());
+	  break;
+	}
+      }
+      else if(cl.is_quantifier())
+	cl = cl.body();
+      else break;
+    }
+  }
+  ast_ref_vector const &pinned = m_ctx.get_pinned();
+  for(unsigned i = 0; i < pinned.size(); i++){
+    ::ast *fa = pinned[i];
+    if(is_func_decl(fa)){
+      ::func_decl *fd = to_func_decl(fa);
+      if(m_ctx.is_predicate(fd)) {
+	func_decl f(_d->ctx,fd);
+	if(!heads.contains(fd)){
+	  int arity = f.arity();
+	  std::vector<expr> args;
+	  for(int j = 0; j < arity; j++)
+	    args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
+	  expr c = implies(_d->ctx.bool_val(false),f(args));
+	  c = _d->ctx.make_quant(Forall,args,c);
+	  clauses.push_back(c);
+	}
+      }
+    }
+  }
+
   // creates 1-1 map between clauses and rpfp edges
   _d->rpfp->FromClauses(clauses);
 
@@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) {
   // dealloc(rs); this is now owned by data
 
   // true means the RPFP problem is SAT, so the query is UNSAT
-  return ans ? l_false : l_true;
+  // but we return undef if the UNSAT result is bounded
+  if(ans){
+    if(rs->IsResultRecursionBounded()){
+#if 0
+      m_ctx.set_status(datalog::BOUNDED);
+      return l_undef;
+#else
+      return l_false;
+#endif
+    }
+    return l_false;
+  }
+  return l_true;
 }
 
 expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 827b90e60..f9916808c 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -252,6 +252,11 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
+	    if(dlctx.get_status() == datalog::BOUNDED){
+	      ctx.regular_stream() << "bounded\n";
+	      print_certificate(ctx);
+	      break;
+	    }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {
             case datalog::INPUT_ERROR:

From 38ee8cb807a5afd9c5b9961d3e7b6213dbbb679f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 22 Aug 2014 12:57:33 +0100
Subject: [PATCH 18/42] .NET API: bugfix. Thanks to Konrad Jamrozik for
 catching this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/update_api.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index f88e0393f..97dacb44b 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -420,7 +420,7 @@ def mk_dotnet():
 
 
 NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
-Unwrapped = [ 'Z3_del_context' ]
+Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
 
 def mk_dotnet_wrappers():
     global Type2Str

From 51aa10821ea54b8c221f6952da146c362edea862 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 26 Aug 2014 13:46:53 -0700
Subject: [PATCH 19/42] fixed pop issue and interpolation proof mode issue

---
 src/cmd_context/interpolant_cmds.cpp | 3 ++-
 src/solver/solver_na2as.cpp          | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index 7fd44c088..cb83b52f6 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -33,6 +33,7 @@ Notes:
 #include"iz3checker.h"
 #include"iz3profiling.h"
 #include"interp_params.hpp"
+#include"scoped_proof.h"
 
 static void show_interpolant_and_maybe_check(cmd_context & ctx,
 					     ptr_vector<ast> &cnsts,
@@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
   ast_manager &_m = ctx.m();
   // TODO: the following is a HACK to enable proofs in the old smt solver
   // When we stop using that solver, this hack can be removed
-  _m.toggle_proof_mode(PGM_FINE);  
+  scoped_proof_mode spm(_m,PGM_FINE);
   ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
   p.set_bool("proof", true);
   scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index 9889b5872..01c45ee44 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) {
 }
 
 void solver_na2as::restore_assumptions(unsigned old_sz) {
-    SASSERT(old_sz == 0);
+  //    SASSERT(old_sz == 0);
     for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
         m_manager.dec_ref(m_assumptions[i]);
     }

From 8ea7109f8fcca01f57e42c625b4c63ecac801bb4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Aug 2014 10:18:42 -0700
Subject: [PATCH 20/42] update documentation to clarify reference counting
 policies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3_api.h | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b9f4975e8..4ffdfa9c2 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1375,6 +1375,16 @@ extern "C" {
        although some parameters can be changed using #Z3_update_param_value.
        All main interaction with Z3 happens in the context of a \c Z3_context.
 
+       In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
+       are determined by the scope level of #Z3_push and #Z3_pop.
+       In other words, a Z3_ast object remains valid until there is a 
+       call to Z3_pop that takes the current scope below the level where 
+       the object was created.
+
+       Note that all other reference counted objects, including Z3_model,
+       Z3_solver, Z3_func_interp have to be managed by the caller. 
+       Their reference counts are not handled by the context.       
+
        \conly \sa Z3_del_context
 
        \conly \deprecated Use #Z3_mk_context_rc

From fa24d9db6fc8598b337795b4d2833c57b242f168 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 1 Sep 2014 17:27:07 +0100
Subject: [PATCH 21/42] Added multi processor compilation to VS project.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/mk_util.py | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 035cdd3c4..5e100b527 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2522,7 +2522,11 @@ def mk_vs_proj(name, components):
     f.write('    <ClCompile>\n')
     f.write('      <Optimization>Disabled</Optimization>\n')
     f.write('      <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
-    f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
+    if VS_PAR:
+        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
+        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
+    else:
+        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
     f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
     f.write('      <WarningLevel>Level3</WarningLevel>\n')
     f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
@@ -2556,7 +2560,11 @@ def mk_vs_proj(name, components):
     f.write('    <ClCompile>\n')
     f.write('      <Optimization>Disabled</Optimization>\n')
     f.write('      <PreprocessorDefinitions>WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
-    f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
+    if VS_PAR:
+        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
+        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
+    else:
+        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
     f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
     f.write('      <WarningLevel>Level3</WarningLevel>\n')
     f.write('      <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')

From 23af977d68ee85a3a1b88d1e59c26bf33f5189df Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 3 Sep 2014 17:49:10 +0100
Subject: [PATCH 22/42] Multi-threading bugfix, DLL could be used from other
 threads before the main thread initializes it. Thanks to user xor88 for
 reporting this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/util/memory_manager.cpp | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 3f2e224d9..45088d5d4 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -35,6 +35,7 @@ static long long  g_memory_max_used_size     = 0;
 static long long  g_memory_watermark         = 0;
 static bool       g_exit_when_out_of_memory  = false;
 static char const * g_out_of_memory_msg      = "ERROR: out of memory";
+static volatile bool g_memory_fully_initialized = false;
 
 void memory::exit_when_out_of_memory(bool flag, char const * msg) {
     g_exit_when_out_of_memory = flag;
@@ -83,10 +84,18 @@ void memory::initialize(size_t max_size) {
             initialize = true;
         }
     }
-    if (!initialize)
-        return;
-    g_memory_out_of_memory  = false;
-    mem_initialize();
+    if (initialize) {
+        g_memory_out_of_memory = false;
+        mem_initialize();
+        g_memory_fully_initialized = true;
+    }
+    else {        
+        // Delay the current thread until the DLL is fully initialized
+        // Without this, multiple threads can start to call API functions
+        // before memory::initialize(...) finishes.
+        while (!g_memory_fully_initialized)
+            /* wait */ ;
+    }
 }
 
 bool memory::is_out_of_memory() {
@@ -98,9 +107,9 @@ bool memory::is_out_of_memory() {
     return r;
 }
 
-void memory::set_high_watermark(size_t watermak) {
+void memory::set_high_watermark(size_t watermark) {
     // This method is only safe to invoke at initialization time, that is, before the threads are created.
-    g_memory_watermark = watermak;
+    g_memory_watermark = watermark;
 }
 
 bool memory::above_high_watermark() {

From 3d9120c74503171c00838f64fe73bb91c3aba821 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Sep 2014 14:49:58 -0700
Subject: [PATCH 23/42] lifetime of expressions from model follow life-time of
 model, not the push/pop scope making scope based reference counting error
 prone

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f17f7a586..f0c31d800 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -60,6 +60,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_expr(r));
         Z3_CATCH_RETURN(0);
     }
@@ -263,6 +264,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_NON_NULL(f, 0);
         expr * e = to_func_interp_ref(f)->get_else();
+        mk_c(c)->save_ast_trail(e);
         RETURN_Z3(of_expr(e));
         Z3_CATCH_RETURN(0);
     }
@@ -301,6 +303,7 @@ extern "C" {
         LOG_Z3_func_entry_get_value(c, e);
         RESET_ERROR_CODE();
         expr * v = to_func_entry_ref(e)->get_result();
+        mk_c(c)->save_ast_trail(v);
         RETURN_Z3(of_expr(v));
         Z3_CATCH_RETURN(0);
     }

From 904ab4bf9e1cf9f147218b88bbfd8ecc8b1a8a0e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Sep 2014 11:18:34 -0700
Subject: [PATCH 24/42] address race condition in cleanup methods

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp              | 10 +++++++--
 src/solver/combined_solver.cpp               | 10 +++++++--
 src/solver/solver.h                          |  4 +++-
 src/solver/tactic2solver.cpp                 |  8 +++++--
 src/tactic/aig/aig.h                         |  2 --
 src/tactic/arith/add_bounds_tactic.cpp       | 10 ++-------
 src/tactic/arith/degree_shift_tactic.cpp     | 10 ++-------
 src/tactic/arith/diff_neq_tactic.cpp         | 13 +++--------
 src/tactic/arith/factor_tactic.cpp           | 10 ++-------
 src/tactic/arith/fix_dl_var_tactic.cpp       | 10 ++-------
 src/tactic/arith/fm_tactic.cpp               | 10 ++-------
 src/tactic/arith/lia2pb_tactic.cpp           | 10 ++-------
 src/tactic/arith/normalize_bounds_tactic.cpp |  9 ++------
 src/tactic/arith/pb2bv_tactic.cpp            |  9 ++------
 src/tactic/arith/propagate_ineqs_tactic.cpp  | 10 ++-------
 src/tactic/arith/recover_01_tactic.cpp       | 10 ++-------
 src/tactic/bv/bit_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv1_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv_size_reduction_tactic.cpp   | 10 ++-------
 src/tactic/bv/max_bv_sharing_tactic.cpp      | 10 ++-------
 src/tactic/core/cofactor_elim_term_ite.cpp   | 23 +++++++-------------
 src/tactic/core/cofactor_elim_term_ite.h     |  3 ++-
 src/tactic/core/ctx_simplify_tactic.cpp      |  9 ++------
 src/tactic/core/der_tactic.cpp               |  9 ++------
 src/tactic/core/elim_term_ite_tactic.cpp     |  9 ++------
 src/tactic/core/elim_uncnstr_tactic.cpp      | 11 +++-------
 src/tactic/core/occf_tactic.cpp              | 10 ++-------
 src/tactic/core/propagate_values_tactic.cpp  |  9 ++------
 src/tactic/core/reduce_args_tactic.cpp       | 11 +++-------
 src/tactic/core/simplify_tactic.cpp          |  9 ++------
 src/tactic/core/simplify_tactic.h            |  4 +++-
 src/tactic/core/solve_eqs_tactic.cpp         | 12 ++++------
 src/tactic/core/tseitin_cnf_tactic.cpp       | 12 +++-------
 src/tactic/fpa/fpa2bv_tactic.cpp             | 12 +++-------
 src/tactic/tactic.h                          |  8 ++++++-
 src/tactic/tactical.cpp                      | 16 +++++---------
 src/tactic/ufbv/macro_finder_tactic.cpp      |  9 ++------
 src/tactic/ufbv/quasi_macros_tactic.cpp      |  9 ++------
 src/tactic/ufbv/ufbv_rewriter_tactic.cpp     |  9 ++------
 39 files changed, 115 insertions(+), 264 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 20539266b..ce2838aba 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver)
-        m_solver->set_cancel(f);
+    if (m_solver) {
+        if (f) {
+            m_solver->cancel(); 
+        }
+        else {
+            m_solver->reset_cancel();
+        }
+    }
     if (has_manager())
         m().set_cancel(f);
 }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index a98e5be49..dfbb62f65 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -218,8 +218,14 @@ public:
     }
 
     virtual void set_cancel(bool f) {
-        m_solver1->set_cancel(f);
-        m_solver2->set_cancel(f);
+        if (f) {
+            m_solver1->cancel();
+            m_solver2->cancel();
+        }
+        else {
+            m_solver1->reset_cancel();
+            m_solver2->reset_cancel();
+        }
     }
     
     virtual void set_progress_callback(progress_callback * callback) {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index e047bace1..a95c649c0 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -99,7 +99,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    virtual void set_cancel(bool f) {}
     /**
        \brief Interrupt this solver.
     */
@@ -130,6 +129,9 @@ public:
        \brief Display the content of this solver.
     */
     virtual void display(std::ostream & out) const;
+protected:
+    virtual void set_cancel(bool f) = 0;
+
 };
 
 #endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 1268fbcea..fb4898ecd 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
 }
 
 void tactic2solver::set_cancel(bool f) {
-    if (m_tactic.get())
-        m_tactic->set_cancel(f);
+    if (m_tactic.get()) {
+        if (f) 
+            m_tactic->cancel();
+        else
+            m_tactic->reset_cancel();
+    }
 }
 
 void tactic2solver::collect_statistics(statistics & st) const {
diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h
index c8befd9b2..291bfbcf3 100644
--- a/src/tactic/aig/aig.h
+++ b/src/tactic/aig/aig.h
@@ -73,8 +73,6 @@ public:
     void display(std::ostream & out, aig_ref const & r) const;
     void display_smt2(std::ostream & out, aig_ref const & r) const;
     unsigned get_num_aigs() const;
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     void set_cancel(bool f);
 };
 
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index d396359a3..9bf967be3 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -172,18 +172,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index a1aa0bdc8..e8fb72be4 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -319,18 +319,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index b534c8295..1a33bf4f2 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -398,20 +398,13 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_conflicts = m_imp->m_num_conflicts;
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
+        d->m_num_conflicts = m_imp->m_num_conflicts;
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_conflicts = num_conflicts;
     }
 
 protected:
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 4eec83037..dc17a4f87 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -333,18 +333,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index d2e3ebf1f..693066ee1 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -338,18 +338,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index c4b7cbaf3..c180029ae 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1682,18 +1682,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
     virtual void operator()(goal_ref const & in, 
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 9ee8f6728..33d5f138e 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -345,18 +345,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index a62b311b5..323903f6c 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -191,17 +191,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 89195a9d5..643195b05 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1002,17 +1002,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 12954005f..d7e4f30d2 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) {
 }
  
 void propagate_ineqs_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        d = m_imp;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel) 
-    {
-        m_imp = d;
-    }
 }
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 3b1a86345..3d222cf56 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -425,18 +425,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 0330141cb..33423c8b1 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -140,18 +140,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 8dcaf2112..5f20015ca 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -465,18 +465,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index d3fdb6e56..e149afc75 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) {
 }
  
 void bv_size_reduction_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index f60487d60..56b18dd8d 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -311,18 +311,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index 1f560ef62..aca6d9084 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const
 }
 
 cofactor_elim_term_ite::~cofactor_elim_term_ite() {
-    imp * d = m_imp;
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        m_imp = 0;
-    }
-    dealloc(d);
+    dealloc(m_imp);
 }
 
 void cofactor_elim_term_ite::updt_params(params_ref const & p) {
@@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
 }
     
 void cofactor_elim_term_ite::set_cancel(bool f) {
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
+    if (m_imp)
+        m_imp->set_cancel(f);
 }
 
 void cofactor_elim_term_ite::cleanup() {
-    ast_manager & m = m_imp->m;
-    #pragma omp critical (cofactor_elim_term_ite) 
+    ast_manager & m = m_imp->m;    
+    imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
     {
-        dealloc(m_imp);
-        m_imp = alloc(imp, m, m_params);
+        std::swap(d, m_imp);
     }
+    dealloc(d);
 }
 
diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h
index ce2f31ea0..e734fcad6 100644
--- a/src/tactic/core/cofactor_elim_term_ite.h
+++ b/src/tactic/core/cofactor_elim_term_ite.h
@@ -37,8 +37,9 @@ public:
     
     void cancel() { set_cancel(true); }
     void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
+    void set_cancel(bool f);
+
 };
 
 #endif
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 71f4771a9..bb38d28ce 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) {
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index c2245b409..2277c3fa8 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -90,17 +90,12 @@ public:
 
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 456bad5e0..e49884004 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -174,17 +174,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 4d64bf061..6d7bcb2f2 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -1036,18 +1036,13 @@ public:
     
     virtual void cleanup() {
         unsigned num_elim_apps = get_num_elim_apps();
-        ast_manager & m = m_imp->m_manager;
-        imp * d = m_imp;
+        ast_manager & m = m_imp->m_manager;        
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
         m_imp->m_num_elim_apps = num_elim_apps;
     }
 
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index f8f6174b9..9b974ae19 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -225,18 +225,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 1e358177f..5873efd61 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -255,17 +255,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 59ed2dcd3..99375e6e8 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -541,17 +541,12 @@ void reduce_args_tactic::set_cancel(bool f) {
 }
 
 void reduce_args_tactic::cleanup() {
-    ast_manager & m   = m_imp->m();
-    imp * d = m_imp;
+    ast_manager & m   = m_imp->m();    
+    imp * d = alloc(imp, m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 95db962a7..39f10e10c 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -115,17 +115,12 @@ void simplify_tactic::set_cancel(bool f) {
 
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
 unsigned simplify_tactic::get_num_steps() const {
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index fc9cb393c..1ba5a6da8 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -43,9 +43,11 @@ public:
     virtual void cleanup();
 
     unsigned get_num_steps() const;
-    virtual void set_cancel(bool f);
 
     virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+protected:
+    virtual void set_cancel(bool f);
+
 };
 
 tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 995940406..3b0a57d20 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -749,23 +749,19 @@ public:
     virtual void cleanup() {
         unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
         expr_replacer * r = m_imp->m_r;
         if (r)
             r->set_substitution(0);
         bool owner = m_imp->m_r_owner;
         m_imp->m_r_owner  = false; // stole replacer
+
+        imp * d = alloc(imp, m, m_params, r, owner);
+        d->m_num_eliminated_vars = num_elim_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, r, owner);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_eliminated_vars = num_elim_vars;
     }
 
     virtual void collect_statistics(statistics & st) const {
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index b6c4b0655..c5be7ab1f 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -898,20 +898,14 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_aux_vars = m_imp->m_num_aux_vars;
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
+        d->m_num_aux_vars = m_imp->m_num_aux_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_aux_vars = num_aux_vars;
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 3a6b7ea45..4a3a01b6f 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -138,19 +138,13 @@ public:
         (*m_imp)(in, result, mc, pc, core);
     }
     
-    virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+    virtual void cleanup() {        
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 80de1bcd0..8b4f9f576 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -47,7 +47,6 @@ public:
 
     void cancel();
     void reset_cancel();
-    virtual void set_cancel(bool f) {}
     
     /**
        \brief Apply tactic to goal \c in.
@@ -96,6 +95,13 @@ public:
 
     // translate tactic to the given manager
     virtual tactic * translate(ast_manager & m) = 0;
+private:
+    friend class nary_tactical;
+    friend class binary_tactical;
+    friend class unary_tactical;
+
+    virtual void set_cancel(bool f) {}
+
 };
 
 typedef ref<tactic>         tactic_ref;
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index ca66b7a14..1e0b07e9d 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -102,11 +102,8 @@ protected:
        \brief Reset cancel flag of t if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -393,11 +390,8 @@ protected:
        \brief Reset cancel flag of st if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -988,7 +982,7 @@ protected:
     virtual void set_cancel(bool f) { 
         m_cancel = f;
         if (m_t) 
-            m_t->set_cancel(f); 
+            m_t->set_cancel(f);
     }
 
     template<typename T>
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 14a42ec51..2f0262fc8 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -144,17 +144,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 393a40603..cea8f2cfc 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -151,17 +151,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 0705c627c..efecb38ba 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -119,17 +119,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

From 36816e3b2fe1c27c97f88a4aaac8f03eb3243a97 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Sep 2014 19:03:37 -0700
Subject: [PATCH 25/42] clear cache for crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp   | 1 +
 src/tactic/sls/sls_tactic.cpp | 9 ++-------
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 94dd5d0a0..d8b96297a 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1221,6 +1221,7 @@ namespace pdr {
             remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
+            m_cache.reset();
         }
     }
 
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index ea5d60668..6783d9621 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -557,17 +557,12 @@ public:
     }
 
     virtual void cleanup() {        
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params, m_stats);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, m_stats);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     virtual void collect_statistics(statistics & st) const {

From dd62ca5eb36c2a62ee44fc5a79fc27c883de21ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Sep 2014 20:54:16 -0700
Subject: [PATCH 26/42] simplify models

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp | 29 ++++++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index d8b96297a..f07964395 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -47,6 +47,7 @@ Notes:
 #include "dl_boogie_proof.h"
 #include "qe_util.h"
 #include "scoped_proof.h"
+#include "expr_safe_replace.h"
 
 namespace pdr {
 
@@ -1062,10 +1063,7 @@ namespace pdr {
             predicates.pop_back();
             for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
                 subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
-                dctx.get_rewriter()(tmp);
-                if (!m.is_true(tmp)) {
-                    constraints.push_back(tmp);
-                }
+                constraints.push_back(tmp);                
             }
             for (unsigned i = 0; i < constraints.size(); ++i) {
                 max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
@@ -1088,7 +1086,28 @@ namespace pdr {
 
             children.append(n->children());
         }            
-        return pm.mk_and(constraints);
+
+        expr_safe_replace repl(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr* e = constraints[i].get(), *e1, *e2;
+            if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
+                repl.insert(e1, e2);
+            }
+            else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
+                repl.insert(e2, e1);
+            }
+        }
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr_ref tmp(m);
+            tmp = constraints[i].get();
+            repl(tmp);
+            dctx.get_rewriter()(tmp);
+            if (!m.is_true(tmp)) {
+                result.push_back(tmp);
+            }
+        }        
+        return pm.mk_and(result);
     }
 
     proof_ref model_search::get_proof_trace(context const& ctx) {

From c917c1c53db30b875a645ba19879a61512d89b17 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Sep 2014 15:54:42 -0700
Subject: [PATCH 27/42] reset ast trail on context deletion

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 05e1ca675..338c12f61 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -128,6 +128,7 @@ namespace api {
             for (unsigned i = 0; i < m_replay_stack.size(); ++i) {
                 dealloc(m_replay_stack[i]);
             }
+            m_ast_trail.reset();
         }
         reset_parser();
         dealloc(m_solver);

From 67b802c9d905329d2411615131b426789cb3856d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Sep 2014 17:38:34 -0700
Subject: [PATCH 28/42] fix scope accounting bug and documentation per Konrad's
 request

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.cpp    | 1 +
 src/api/api_solver_old.cpp | 2 +-
 src/api/z3_api.h           | 7 ++++++-
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 338c12f61..3349bed7c 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -361,6 +361,7 @@ namespace api {
                 }
             }
         }
+        SASSERT(num_scopes <= get_smt_kernel().get_scope_level());
         get_smt_kernel().pop(num_scopes);
     }
 
diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp
index e0533fbd9..b81fb2f2c 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -40,7 +40,7 @@ extern "C" {
         LOG_Z3_pop(c, num_scopes);
         RESET_ERROR_CODE();
         CHECK_SEARCHING(c);
-        if (num_scopes > mk_c(c)->get_smt_kernel().get_scope_level()) {
+        if (num_scopes > mk_c(c)->get_num_scopes()) {
             SET_ERROR_CODE(Z3_IOB);
             return;
         }
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 4ffdfa9c2..e1c42667a 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7069,7 +7069,7 @@ END_MLAPI_EXCLUDE
        \mlonly then a valid model is returned.  Otherwise, it is unsafe to use the returned model.\endmlonly
        \conly The caller is responsible for deleting the model using the function #Z3_del_model.
        
-       \conly \remark In constrast with the rest of the Z3 API, the reference counter of the
+       \conly \remark In contrast with the rest of the Z3 API, the reference counter of the
        \conly model is incremented. This is to guarantee backward compatibility. In previous
        \conly versions, models did not support reference counting.
        
@@ -7182,6 +7182,11 @@ END_MLAPI_EXCLUDE
        \brief Delete a model object.
        
        \sa Z3_check_and_get_model
+
+       \conly \remark The Z3_check_and_get_model automatically increments a reference count on the model.
+       \conly The expected usage is that models created by that method are deleted using Z3_del_model.
+       \conly This is for backwards compatibility and in contrast to the rest of the API where
+       \conly callers are responsible for managing reference counts.
     
        \deprecated Subsumed by Z3_solver API
        

From 919e0a5ea2f2bef4fe8ab9880e91dd52a7fc2bd1 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 16 Sep 2014 14:56:59 +0100
Subject: [PATCH 29/42] Z3Py: fix bug in substitute() with a list of on
 variable e.g. print substitute(Int('x'), [(Int('x'), Int('y'))])

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/api/python/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 50d29a790..d46d40ab2 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6960,7 +6960,7 @@ def substitute(t, *m):
     if isinstance(m, tuple):
         m1 = _get_args(m)
         if isinstance(m1, list):
-            m = _get_args(m1)
+            m = m1
     if __debug__:
         _z3_assert(is_expr(t), "Z3 expression expected")
         _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")

From f7c3559c31b5d5c7335706a61a7f9c6e47a55545 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 16 Sep 2014 15:26:01 +0100
Subject: [PATCH 30/42] fix a few compiler warnings

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/api/api_interp.cpp             | 2 +-
 src/muz/pdr/pdr_farkas_learner.cpp | 1 -
 src/smt/smt_model_checker.cpp      | 3 +--
 3 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 03d5ff843..e06ad5192 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -411,7 +411,7 @@ static void get_file_params(const char *filename, hash_map<std::string,std::stri
       for(unsigned i = 0; i < tokens.size(); i++){
 	std::string &tok = tokens[i];
 	size_t eqpos = tok.find('=');
-	if(eqpos >= 0 && eqpos < tok.size()){
+	if(eqpos != std::string::npos){
 	  std::string left = tok.substr(0,eqpos);
 	  std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1);
 	  params[left] = right;
diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index 7c38bf86f..b440ef519 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -905,7 +905,6 @@ namespace pdr {
     void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas) {
         ast_manager& m = lemmas.get_manager();
         ast_mark visited;
-        proof* p0 = p;
         ptr_vector<proof> todo;        
         todo.push_back(p);
                       
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 526447f9f..7053d63ec 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -136,9 +136,8 @@ namespace smt {
         if (cex == 0)
             return false; // no model available.
         unsigned num_decls = q->get_num_decls();
-        unsigned   num_sks = sks.size();
         // Remark: sks were created for the flat version of q.
-        SASSERT(num_sks >= num_decls); 
+        SASSERT(sks.size() >= num_decls);
         expr_ref_buffer bindings(m_manager);
         bindings.resize(num_decls);
         unsigned max_generation = 0;

From 79326e24dfb9dff723d1ce64b3f50bcf394bd48c Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 16 Sep 2014 15:29:25 +0100
Subject: [PATCH 31/42] fix debug build..

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/pdr/pdr_farkas_learner.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index b440ef519..7c38bf86f 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -905,6 +905,7 @@ namespace pdr {
     void farkas_learner::get_asserted(proof* p, expr_set const& bs, ast_mark& b_closed, obj_hashtable<expr>& lemma_set, expr_ref_vector& lemmas) {
         ast_manager& m = lemmas.get_manager();
         ast_mark visited;
+        proof* p0 = p;
         ptr_vector<proof> todo;        
         todo.push_back(p);
                       

From d01ca110012a7f92495bf37827df641a2d6378db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Sep 2014 17:13:09 -0700
Subject: [PATCH 32/42] reduce asymptotic overhead of asserting bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.cpp |   8 +-
 src/smt/theory_arith.h      |  17 +++
 src/smt/theory_arith_core.h | 264 ++++++++++++++++++++++++++++++++----
 3 files changed, 259 insertions(+), 30 deletions(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index fbef46ae3..3d0c7c880 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1104,10 +1104,10 @@ namespace datalog {
    
     void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
-	  expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
-	  rules.push_back(r.get());
-	  //            rules.push_back(m_rule_fmls[i].get());
-	  names.push_back(m_rule_names[i]);
+            expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
+            rules.push_back(r.get());
+            //            rules.push_back(m_rule_fmls[i].get());
+            names.push_back(m_rule_names[i]);
         }
     }
 
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 998dd72e6..d1af762bb 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -410,6 +410,7 @@ namespace smt {
         atoms                   m_atoms;            // set of theory atoms
         ptr_vector<bound>       m_asserted_bounds;  // set of asserted bounds
         unsigned                m_asserted_qhead;   
+        ptr_vector<atom>        m_new_atoms;        // new bound atoms that have yet to be internalized.
         svector<theory_var>     m_nl_monomials;     // non linear monomials
         svector<theory_var>     m_nl_propagated;    // non linear monomials that became linear
         v_dependency_manager    m_dep_manager;      // for tracking bounds during non-linear reasoning
@@ -570,6 +571,22 @@ namespace smt {
         void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params);
         void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params);
         void mk_bound_axioms(atom * a);
+        void mk_bound_axiom(atom* a1, atom* a2);
+        void flush_bound_axioms();
+        typename atoms::iterator next_sup(atom* a1, atom_kind kind, 
+                                          typename atoms::iterator it, 
+                                          typename atoms::iterator end,
+                                          bool& found_compatible);
+        typename atoms::iterator next_inf(atom* a1, atom_kind kind, 
+                                          typename atoms::iterator it, 
+                                          typename atoms::iterator end,
+                                          bool& found_compatible);
+        typename atoms::iterator first(atom_kind kind, 
+                                       typename atoms::iterator it, 
+                                       typename atoms::iterator end);
+        struct compare_atoms {
+            bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); }
+        };
         virtual bool default_internalizer() const { return false; }
         virtual bool internalize_atom(app * n, bool gate_ctx);
         virtual bool internalize_term(app * term);
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index fbc043048..ba4eefc36 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -348,13 +348,24 @@ namespace smt {
         context & ctx   = get_context();
         simplifier & s  = ctx.get_simplifier();
         expr_ref s_ante(m), s_conseq(m);
+        expr* s_conseq_n, * s_ante_n;
+        bool negated;
         proof_ref pr(m);
+
         s(ante, s_ante, pr);
+        negated = m.is_not(s_ante, s_ante_n);
+        if (negated) s_ante = s_ante_n;
         ctx.internalize(s_ante, false);
         literal l_ante = ctx.get_literal(s_ante);
+        if (negated) l_ante.neg();
+
         s(conseq, s_conseq, pr);
+        negated = m.is_not(s_conseq, s_conseq_n);
+        if (negated) s_conseq = s_conseq_n;
         ctx.internalize(s_conseq, false);
         literal l_conseq = ctx.get_literal(s_conseq);
+        if (negated) l_conseq.neg();
+
         literal lits[2] = {l_ante, l_conseq};
         ctx.mk_th_axiom(get_id(), 2, lits);
         if (ctx.relevancy()) {
@@ -800,48 +811,244 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::mk_bound_axioms(atom * a1) {
         theory_var v = a1->get_var();
-        literal   l1(a1->get_bool_var()); 
+        atoms & occs = m_var_occs[v];
+        if (!get_context().is_searching()) {
+            //
+            // NB. We make an assumption that user push calls propagation 
+            // before internal scopes are pushed. This flushes all newly 
+            // asserted atoms into the right context.
+            //
+            m_new_atoms.push_back(a1);
+            return;
+        }
         numeral const & k1(a1->get_k());
         atom_kind kind1 = a1->get_atom_kind();
         TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";);
-        atoms & occs = m_var_occs[v];
         typename atoms::iterator it  = occs.begin();
         typename atoms::iterator end = occs.end();
+
+        typename atoms::iterator lo_inf = end, lo_sup = end;
+        typename atoms::iterator hi_inf = end, hi_sup = end;
         for (; it != end; ++it) {
-            atom * a2 = *it;
-            literal l2(a2->get_bool_var());
-            numeral const & k2 = a2->get_k();
-            atom_kind kind2    = a2->get_atom_kind();
+            atom * a2 = *it;            
+            numeral const & k2(a2->get_k());
+            atom_kind kind2 = a2->get_atom_kind();
             SASSERT(k1 != k2 || kind1 != kind2);
-            SASSERT(a2->get_var() == v);
-            parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) };
-            if (kind1 == A_LOWER) {
-                if (kind2 == A_LOWER) {
-                    // x >= k1, x >= k2 
-                    if (k1 >= k2) mk_clause(~l1, l2, 3, coeffs);
-                    else mk_clause(~l2, l1, 3, coeffs);
+            if (kind2 == A_LOWER) {
+                if (k2 < k1) {
+                    if (lo_inf == end || k2 > (*lo_inf)->get_k()) {
+                        lo_inf = it;
+                    }
                 }
-                else {
-                    // x >= k1, x <= k2      
-                    if (k1 > k2) mk_clause(~l1, ~l2, 3, coeffs);
-                    else mk_clause(l1, l2, 3, coeffs);
+                else if (lo_sup == end || k2 < (*lo_sup)->get_k()) {
+                    lo_sup = it;
                 }
             }
-            else {
-                if (kind2 == A_LOWER) {
-                    // x <= k1, x >= k2
-                    if (k1 < k2) mk_clause(~l1, ~l2, 3, coeffs);
-                    else mk_clause(l1, l2, 3, coeffs);
+            else if (k2 < k1) {
+                if (hi_inf == end || k2 > (*hi_inf)->get_k()) {
+                    hi_inf = it;
+                }
+            }
+            else if (hi_sup == end || k2 < (*hi_sup)->get_k()) {
+                hi_sup = it;
+            }
+        }        
+        if (lo_inf != end) mk_bound_axiom(a1, *lo_inf);
+        if (lo_sup != end) mk_bound_axiom(a1, *lo_sup);
+        if (hi_inf != end) mk_bound_axiom(a1, *hi_inf);
+        if (hi_sup != end) mk_bound_axiom(a1, *hi_sup);
+    }
+
+    template<typename Ext>
+    void theory_arith<Ext>::mk_bound_axiom(atom* a1, atom* a2) {
+        theory_var v = a1->get_var();
+        literal   l1(a1->get_bool_var()); 
+        literal   l2(a2->get_bool_var()); 
+        numeral const & k1(a1->get_k());
+        numeral const & k2(a2->get_k());
+        atom_kind kind1 = a1->get_atom_kind();
+        atom_kind kind2 = a2->get_atom_kind();
+        bool v_is_int = is_int(v);
+        SASSERT(v == a2->get_var());
+        SASSERT(k1 != k2 || kind1 != kind2);
+        parameter coeffs[3] = { parameter(symbol("farkas")), 
+                                parameter(rational(1)), parameter(rational(1)) };
+
+        //std::cout << "v" << v << " " << ((kind1==A_LOWER)?"<= ":">= ") << k1 << "\t    ";
+        //std::cout << "v" << v << " " << ((kind2==A_LOWER)?"<= ":">= ") << k2 << "\n";
+
+        if (kind1 == A_LOWER) {
+            if (kind2 == A_LOWER) {
+                if (k2 <= k1) {
+                    mk_clause(~l1, l2, 3, coeffs);
                 }
                 else {
-                    // x <= k1, x <= k2
-                    if (k1 < k2) mk_clause(~l1, l2, 3, coeffs);
-                    else mk_clause(~l2, l1, 3, coeffs);
+                    mk_clause(l1, ~l2, 3, coeffs);
+                }
+            }
+            else if (k1 <= k2) {
+                // k1 <= k2, k1 <= x or x <= k2
+                mk_clause(l1, l2, 3, coeffs);
+            }
+            else {
+                // k1 > hi_inf, k1 <= x => ~(x <= hi_inf)
+                mk_clause(~l1, ~l2, 3, coeffs);
+                if (v_is_int && k1 == k2 + numeral(1)) {
+                    // k1 <= x or x <= k1-1
+                    mk_clause(l1, l2, 3, coeffs);
                 }
             }
         }
+        else if (kind2 == A_LOWER) {
+            if (k1 >= k2) {
+                // k1 >= lo_inf, k1 >= x or lo_inf <= x
+                mk_clause(l1, l2, 3, coeffs);
+            }
+            else {
+                // k1 < k2, k2 <= x => ~(x <= k1)
+                mk_clause(~l1, ~l2, 3, coeffs); 
+                if (v_is_int && k1 == k2 - numeral(1)) {
+                    // x <= k1 or k1+l <= x
+                    mk_clause(l1, l2, 3, coeffs);
+                }
+
+            }
+        }
+        else {
+            // kind1 == A_UPPER, kind2 == A_UPPER
+            if (k1 >= k2) {
+                // k1 >= k2, x <= k2 => x <= k1
+                mk_clause(l1, ~l2, 3, coeffs);
+            }
+            else {
+                // k1 <= hi_sup , x <= k1 =>  x <= hi_sup
+                mk_clause(~l1, l2, 3, coeffs);
+            }
+        }        
     }
 
+    template<typename Ext>
+    void theory_arith<Ext>::flush_bound_axioms() {
+        while (!m_new_atoms.empty()) {
+            ptr_vector<atom> atoms;            
+            atoms.push_back(m_new_atoms.back());
+            m_new_atoms.pop_back();
+            theory_var v = atoms.back()->get_var();
+            for (unsigned i = 0; i < m_new_atoms.size(); ++i) {
+                if (m_new_atoms[i]->get_var() == v) {
+                    atoms.push_back(m_new_atoms[i]);
+                    m_new_atoms[i] = m_new_atoms.back();
+                    m_new_atoms.pop_back();
+                    --i;
+                }
+            }            
+            ptr_vector<atom> occs(m_var_occs[v]);
+
+            std::sort(atoms.begin(), atoms.end(), compare_atoms());
+            std::sort(occs.begin(), occs.end(), compare_atoms());
+
+            typename atoms::iterator begin1 = occs.begin();
+            typename atoms::iterator begin2 = occs.begin();
+            typename atoms::iterator end = occs.end();
+            begin1 = first(A_LOWER, begin1, end);
+            begin2 = first(A_UPPER, begin2, end);
+
+            typename atoms::iterator lo_inf = begin1, lo_sup = begin1;
+            typename atoms::iterator hi_inf = begin2, hi_sup = begin2;
+            typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1;
+            typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
+            bool flo_inf, fhi_inf, flo_sup, fhi_sup;
+   //         std::cout << atoms.size() << "\n";
+            ptr_addr_hashtable<typename atom> visited;
+            for (unsigned i = 0; i < atoms.size(); ++i) {
+                atom* a1 = atoms[i];
+                lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf);
+                hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf);
+                lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup);
+                hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup);
+//                std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n";
+ //               std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n";
+                if (lo_inf1 != end) lo_inf = lo_inf1; 
+                if (lo_sup1 != end) lo_sup = lo_sup1; 
+                if (hi_inf1 != end) hi_inf = hi_inf1; 
+                if (hi_sup1 != end) hi_sup = hi_sup1; 
+                if (!flo_inf) lo_inf = end;
+                if (!fhi_inf) hi_inf = end;
+                if (!flo_sup) lo_sup = end;
+                if (!fhi_sup) hi_sup = end;
+                visited.insert(a1);
+                if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(a1, *lo_inf);
+                if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(a1, *lo_sup);
+                if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(a1, *hi_inf);
+                if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(a1, *hi_sup);
+            }                            
+        }
+    }
+
+    template<typename Ext>
+    typename theory_arith<Ext>::atoms::iterator 
+    theory_arith<Ext>::first(
+        atom_kind kind, 
+        typename atoms::iterator it, 
+        typename atoms::iterator end) {
+        for (; it != end; ++it) {
+            atom* a = *it;
+            if (a->get_atom_kind() == kind) return it;
+        }
+        return end;
+    }
+
+    template<typename Ext>
+    typename theory_arith<Ext>::atoms::iterator 
+    theory_arith<Ext>::next_inf(
+        atom* a1, 
+        atom_kind kind, 
+        typename atoms::iterator it, 
+        typename atoms::iterator end,
+        bool& found_compatible) {
+        numeral const & k1(a1->get_k());
+        typename atoms::iterator result = end;
+        found_compatible = false;
+        for (; it != end; ++it) {
+            atom * a2 = *it;            
+            if (a1 == a2) continue;
+            if (a2->get_atom_kind() != kind) continue;
+            numeral const & k2(a2->get_k());
+            found_compatible = true;
+            if (k2 <= k1) {
+                result = it;
+            }
+            else {
+                break;
+            }
+        }
+        return result;
+    }
+
+    template<typename Ext>
+    typename theory_arith<Ext>::atoms::iterator 
+    theory_arith<Ext>::next_sup(
+        atom* a1, 
+        atom_kind kind, 
+        typename atoms::iterator it, 
+        typename atoms::iterator end,
+        bool& found_compatible) {
+        numeral const & k1(a1->get_k());
+        found_compatible = false;
+        for (; it != end; ++it) {
+            atom * a2 = *it;            
+            if (a1 == a2) continue;
+            if (a2->get_atom_kind() != kind) continue;
+            numeral const & k2(a2->get_k());
+            found_compatible = true;
+            if (k1 < k2) {
+                return it;
+            }
+        }
+        return end;
+    }
+
+
     template<typename Ext>
     bool theory_arith<Ext>::internalize_atom(app * n, bool gate_ctx) {
         TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
@@ -879,7 +1086,7 @@ namespace smt {
         bool_var bv    = ctx.mk_bool_var(n);
         ctx.set_var_theory(bv, get_id());
         rational _k;
-        m_util.is_numeral(rhs, _k);
+        VERIFY(m_util.is_numeral(rhs, _k));
         numeral   k(_k);
         atom * a = alloc(atom, bv, v, k, kind);
         mk_bound_axioms(a);
@@ -927,6 +1134,7 @@ namespace smt {
     
     template<typename Ext>
     void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
+        TRACE("arith", tout << "v" << v << " " << is_true << "\n";);
         atom * a = get_bv2a(v);
         if (!a) return;
         SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@@ -1142,6 +1350,7 @@ namespace smt {
         CASSERT("arith", wf_columns());
         CASSERT("arith", valid_row_assignment());
         
+        flush_bound_axioms();
         propagate_linear_monomials();
         while (m_asserted_qhead < m_asserted_bounds.size()) {
             bound * b = m_asserted_bounds[m_asserted_qhead];
@@ -2421,6 +2630,8 @@ namespace smt {
                     if (val == l_undef)
                         continue;
                     // TODO: check if the following line is a bottleneck
+                    TRACE("arith", tout << "v" << a->get_bool_var() << " " << (val == l_true) << "\n";);
+
                     a->assign_eh(val == l_true, get_epsilon(a->get_var()));
                     if (val != l_undef && a->get_bound_kind() == b->get_bound_kind()) {
                         SASSERT((ctx.get_assignment(bv) == l_true) == a->is_true());
@@ -2916,6 +3127,7 @@ namespace smt {
         SASSERT(m_to_patch.empty());
         m_to_check.reset();
         m_in_to_check.reset();
+        m_new_atoms.reset();
         CASSERT("arith", wf_rows());
         CASSERT("arith", wf_columns());
         CASSERT("arith", valid_row_assignment());

From 1636e35bf99443d4186f9a4b9c7f828b2aa9502d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Sep 2014 20:11:44 -0700
Subject: [PATCH 33/42] fix scope accounting bug in deprecated solver mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.cpp | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 3349bed7c..b10621d43 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -343,22 +343,18 @@ namespace api {
     
     void context::push() {
         get_smt_kernel().push();
-        if (!m_user_ref_count) {
-            m_ast_lim.push_back(m_ast_trail.size());
-            m_replay_stack.push_back(0);
-        }
+        m_ast_lim.push_back(m_ast_trail.size());
+        m_replay_stack.push_back(0);        
     }
     
     void context::pop(unsigned num_scopes) {
         for (unsigned i = 0; i < num_scopes; ++i) {
-            if (!m_user_ref_count) {
-                unsigned sz = m_ast_lim.back();
-                m_ast_lim.pop_back();
-                dealloc(m_replay_stack.back());
-                m_replay_stack.pop_back();
-                while (m_ast_trail.size() > sz) {
-                    m_ast_trail.pop_back();
-                }
+            unsigned sz = m_ast_lim.back();
+            m_ast_lim.pop_back();
+            dealloc(m_replay_stack.back());
+            m_replay_stack.pop_back();
+            while (m_ast_trail.size() > sz) {
+                m_ast_trail.pop_back();
             }
         }
         SASSERT(num_scopes <= get_smt_kernel().get_scope_level());

From a85f1784db95c5975c3484215407f985d19f61ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Sep 2014 23:25:39 -0700
Subject: [PATCH 34/42] updated answer to binary interpolant

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index d46d40ab2..879b19597 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7344,7 +7344,7 @@ def binary_interpolant(a,b,p=None,ctx=None):
 
     >>> x = Int('x')
     >>> print binary_interpolant(x<0,x>2)
-    x <= 2
+    Not(x >= 0)
     """
     f = And(Interp(a),b)
     return tree_interpolant(f,p,ctx)[0]

From b95f5b0fea8f239d45ffaf88615c400339ca1101 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Wed, 17 Sep 2014 16:33:27 +0100
Subject: [PATCH 35/42] fix bug in the datalog compiler when using negation We
 now perform negation after filtering with interpreted constraints so that the
 table reflects relevant columns which were not being added by the negation

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/dl_compiler.cpp | 84 ++++++++++++++++++-------------------
 1 file changed, 42 insertions(+), 42 deletions(-)

diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index 276e7b836..2a2507d7f 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -589,49 +589,8 @@ namespace datalog {
             dealloc = true;
         }
 
-        //enforce negative predicates
-        unsigned ut_len=r->get_uninterpreted_tail_size();
-        for(unsigned i=pt_len; i<ut_len; i++) {
-            app * neg_tail = r->get_tail(i);
-            func_decl * neg_pred = neg_tail->get_decl();
-            variable_intersection neg_intersection(m_context.get_manager());
-            neg_intersection.populate(single_res_expr, neg_tail);
-            unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1());
-            unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2());
-
-            unsigned neg_len = neg_tail->get_num_args();
-            for(unsigned i=0; i<neg_len; i++) {
-                expr * e = neg_tail->get_arg(i);
-                if(is_var(e)) {
-                    continue;
-                }
-                SASSERT(is_app(e));
-                relation_sort arg_sort;
-                m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
-                reg_idx new_reg;
-                bool new_dealloc;
-                make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
-
-                if (dealloc)
-                    make_dealloc_non_void(filtered_res, acc);
-                dealloc = new_dealloc;
-                filtered_res = new_reg;                // here filtered_res value gets changed !!
-
-                t_cols.push_back(single_res_expr.size());
-                neg_cols.push_back(i);
-                single_res_expr.push_back(e);
-            }
-            SASSERT(t_cols.size()==neg_cols.size());
-
-            reg_idx neg_reg = m_pred_regs.find(neg_pred);
-            if (!dealloc)
-                make_clone(filtered_res, filtered_res, acc);
-            acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
-                t_cols.c_ptr(), neg_cols.c_ptr()));
-            dealloc = true;
-        }
-
         // enforce interpreted tail predicates
+        unsigned ut_len = r->get_uninterpreted_tail_size();
         unsigned ft_len = r->get_tail_size(); // full tail
         ptr_vector<expr> tail;
         for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) {
@@ -738,6 +697,47 @@ namespace datalog {
             dealloc = true;
         }
 
+        //enforce negative predicates
+        for (unsigned i = pt_len; i<ut_len; i++) {
+            app * neg_tail = r->get_tail(i);
+            func_decl * neg_pred = neg_tail->get_decl();
+            variable_intersection neg_intersection(m_context.get_manager());
+            neg_intersection.populate(single_res_expr, neg_tail);
+            unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1());
+            unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2());
+
+            unsigned neg_len = neg_tail->get_num_args();
+            for (unsigned i = 0; i<neg_len; i++) {
+                expr * e = neg_tail->get_arg(i);
+                if (is_var(e)) {
+                    continue;
+                }
+                SASSERT(is_app(e));
+                relation_sort arg_sort;
+                m_context.get_rel_context()->get_rmanager().from_predicate(neg_pred, i, arg_sort);
+                reg_idx new_reg;
+                bool new_dealloc;
+                make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc);
+
+                if (dealloc)
+                    make_dealloc_non_void(filtered_res, acc);
+                dealloc = new_dealloc;
+                filtered_res = new_reg;                // here filtered_res value gets changed !!
+
+                t_cols.push_back(single_res_expr.size());
+                neg_cols.push_back(i);
+                single_res_expr.push_back(e);
+            }
+            SASSERT(t_cols.size() == neg_cols.size());
+
+            reg_idx neg_reg = m_pred_regs.find(neg_pred);
+            if (!dealloc)
+                make_clone(filtered_res, filtered_res, acc);
+            acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(),
+                t_cols.c_ptr(), neg_cols.c_ptr()));
+            dealloc = true;
+        }
+
 #if 0
         // this version is potentially better for non-symbolic tables,
         // since it constraints each unbound column at a time (reducing the

From 45bfcda16cd209f565b0dad6518b0179b2cb7057 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Sep 2014 16:37:53 -0700
Subject: [PATCH 36/42] remove typename

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_core.h | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index ba4eefc36..c743562da 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -874,9 +874,6 @@ namespace smt {
         parameter coeffs[3] = { parameter(symbol("farkas")), 
                                 parameter(rational(1)), parameter(rational(1)) };
 
-        //std::cout << "v" << v << " " << ((kind1==A_LOWER)?"<= ":">= ") << k1 << "\t    ";
-        //std::cout << "v" << v << " " << ((kind2==A_LOWER)?"<= ":">= ") << k2 << "\n";
-
         if (kind1 == A_LOWER) {
             if (kind2 == A_LOWER) {
                 if (k2 <= k1) {
@@ -958,16 +955,13 @@ namespace smt {
             typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1;
             typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2;
             bool flo_inf, fhi_inf, flo_sup, fhi_sup;
-   //         std::cout << atoms.size() << "\n";
-            ptr_addr_hashtable<typename atom> visited;
+            ptr_addr_hashtable<atom> visited;
             for (unsigned i = 0; i < atoms.size(); ++i) {
                 atom* a1 = atoms[i];
                 lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf);
                 hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf);
                 lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup);
                 hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup);
-//                std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n";
- //               std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n";
                 if (lo_inf1 != end) lo_inf = lo_inf1; 
                 if (lo_sup1 != end) lo_sup = lo_sup1; 
                 if (hi_inf1 != end) hi_inf = hi_inf1; 

From 61d67dc2dee3270919caf883128f3a655b18f5c9 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Thu, 18 Sep 2014 14:38:40 +0100
Subject: [PATCH 37/42] fix a few compiler warnings

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/dl_vector_relation.h | 2 --
 src/util/debug.h                 | 2 +-
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/muz/rel/dl_vector_relation.h b/src/muz/rel/dl_vector_relation.h
index 114f4ca43..4d0917359 100644
--- a/src/muz/rel/dl_vector_relation.h
+++ b/src/muz/rel/dl_vector_relation.h
@@ -62,8 +62,6 @@ namespace datalog {
             dealloc(m_elems);
         }
 
-        virtual bool can_swap() const { return true; }
-
         virtual void swap(relation_base& other) {
             vector_relation& o = dynamic_cast<vector_relation&>(other);
             if (&o == this) return;
diff --git a/src/util/debug.h b/src/util/debug.h
index 9e519982f..a36743f73 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -73,7 +73,7 @@ bool is_debug_enabled(const char * tag);
         UNREACHABLE();                                          \
     }                                                           
 #else
-#define VERIFY(_x_) (_x_)
+#define VERIFY(_x_) (void)(_x_)
 #endif
 
 #define MAKE_NAME2(LINE) zofty_ ## LINE 

From 9949c7e31c8dae78dcf7dc44eabc8157981c0310 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 18 Sep 2014 17:09:22 +0100
Subject: [PATCH 38/42] fixed typos

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/mk_util.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 5e100b527..411fdd1e1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -455,7 +455,7 @@ def display_help(exit_code):
         print("  -v, --vsproj                  generate Visual Studio Project Files.")
     if IS_WINDOWS:
         print("  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules.")
-    print("  -j, --java                    generate Java bindinds.")
+    print("  -j, --java                    generate Java bindings.")
     print("  --staticlib                   build Z3 static library.")
     if not IS_WINDOWS:
         print("  -g, --gmp                     use GMP.")
@@ -587,7 +587,7 @@ def set_z3py_dir(p):
         raise MKException("Python bindings directory '%s' does not exist" % full)
     Z3PY_SRC_DIR = full
     if VERBOSE:
-        print("Python bindinds directory was detected.")
+        print("Python bindings directory was detected.")
 
 _UNIQ_ID = 0
 

From d36cecc2f328cdd742c601cee6bc803dca1b2b14 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Fri, 19 Sep 2014 15:51:08 +0100
Subject: [PATCH 39/42] make use of count population intrinsincs on
 MSVC/gcc/clang

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/util/util.h | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/util/util.h b/src/util/util.h
index 0aa8f881d..58120b2f2 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -95,7 +95,12 @@ unsigned uint64_log2(uint64 v);
 COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
 
 // Return the number of 1 bits in v.
-inline unsigned get_num_1bits(unsigned v) {
+static inline unsigned get_num_1bits(unsigned v) {
+#ifdef _MSC_VER
+    return __popcnt(v);
+#elif defined(__GNUC__)
+    return __builtin_popcount(v);
+#else
 #ifdef Z3DEBUG
     unsigned c;
     unsigned v1 = v;
@@ -108,15 +113,16 @@ inline unsigned get_num_1bits(unsigned v) {
     unsigned r = (((v + (v >> 4)) & 0xF0F0F0F) * 0x1010101) >> 24; 
     SASSERT(c == r);
     return r;
+#endif
 }
 
 // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64.
 // So, I'm using the following two definitions to fix the problem
-inline uint64 shift_right(uint64 x, uint64 y) {
+static inline uint64 shift_right(uint64 x, uint64 y) {
     return y < 64ull ? (x >> y) : 0ull;
 }
 
-inline uint64 shift_left(uint64 x, uint64 y) {
+static inline uint64 shift_left(uint64 x, uint64 y) {
     return y < 64ull ? (x << y) : 0ull;
 }
 
@@ -255,10 +261,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair<T1, T2> const & p
     return out;
 }
 
-#ifndef _WINDOWS
-#define __forceinline inline
-#endif
-
 template<typename IT>
 bool has_duplicates(const IT & begin, const IT & end) {
     for (IT it1 = begin; it1 != end; ++it1) {

From b243ac945f7e87fe669b9527d6f6c0e705cfe666 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Sun, 21 Sep 2014 15:20:43 +0100
Subject: [PATCH 40/42] hoprfully fix the build for MSVC 2010

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/util/util.h | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/util/util.h b/src/util/util.h
index 58120b2f2..eb24ece13 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -24,6 +24,9 @@ Revision History:
 #include<iostream>
 #include<climits>
 #include<limits>
+#ifdef _MSC_VER
+#include<intrin.h>
+#endif
 
 #ifndef SIZE_MAX
 #define SIZE_MAX std::numeric_limits<std::size_t>::max()

From dca3ce6b24f1a8752bf0a7252c2eaf1bb888d5ba Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Sep 2014 01:16:16 -0700
Subject: [PATCH 41/42] update documentation on models associated with solver
 objects

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3_api.h | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index e1c42667a..b561b6bf1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6620,6 +6620,13 @@ END_MLAPI_EXCLUDE
     /**
        \brief Create a new (incremental) solver.
 
+       The function #Z3_solver_get_model retrieves a model if the
+       assertions is satisfiable (i.e., the result is \c
+       Z3_L_TRUE) and model construction is enabled.
+       The function #Z3_solver_get_model can also be used even
+       if the result is \c Z3_L_UNDEF, but the returned model
+       is not guaranteed to satisfy quantified assertions.
+
        def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
     */
     Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c);
@@ -6757,8 +6764,11 @@ END_MLAPI_EXCLUDE
        \brief Check whether the assertions in a given solver are consistent or not.
 
        The function #Z3_solver_get_model retrieves a model if the
-       assertions are not unsatisfiable (i.e., the result is not \c
-       Z3_L_FALSE) and model construction is enabled.
+       assertions is satisfiable (i.e., the result is \c
+       Z3_L_TRUE) and model construction is enabled.
+       Note that if the call returns Z3_L_UNDEF, Z3 does not
+       ensure that calls to #Z3_solver_get_model succeed and any models
+       produced in this case are not guaranteed to satisfy the assertions.
 
        The function #Z3_solver_get_proof retrieves a proof if proof
        generation was enabled when the context was created, and the 

From 4995ce1fdee47ffd61d4726c89ff908f468d6450 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Sep 2014 22:22:26 -0700
Subject: [PATCH 42/42] disable unstable interpolation sample

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 879b19597..b6cceeb8e 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7342,8 +7342,8 @@ def binary_interpolant(a,b,p=None,ctx=None):
     If parameters p are supplied, these are used in creating the
     solver that determines satisfiability.
 
-    >>> x = Int('x')
-    >>> print binary_interpolant(x<0,x>2)
+    x = Int('x')
+    print binary_interpolant(x<0,x>2)
     Not(x >= 0)
     """
     f = And(Interp(a),b)