add colors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.8.11.0 LANGUAGES CXX C)
+project(Z3 VERSION 4.8.12.0 LANGUAGES CXX C)
 
 ################################################################################
 # Project version

RELEASE_NOTES

@@ -10,6 +10,7 @@ Version 4.8.next
     option, but at this point does not translate into benefits. It is currently 
     turned off by default.
 
+
 Version 4.8.11
 ==============
   - self-contained character theory, direct support for UTF8, Unicode character sets.

scripts/mk_consts_files.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+# -- /usr/bin/env python
 """
 Reads a list of Z3 API header files and
 generate the constant declarations need

scripts/mk_def_file.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#  - /usr/bin/env python
 """
 Reads a list of Z3 API header files and
 generate a ``.def`` file to define the

scripts/mk_gparams_register_modules_cpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+# -- /usr/bin/env python
 """
 Determines the available global parameters from a list of header files and
 generates a ``gparams_register_modules.cpp`` file in the destination directory

scripts/mk_install_tactic_cpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+# -- /usr/bin/env python
 """
 Determines the available tactics from a list of header files and generates a
 ``install_tactic.cpp`` file in the destination directory that defines a

scripts/mk_mem_initializer_cpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+# -- /usr/bin/env python
 """
 Scans the listed header files for
 memory initializers and finalizers and

scripts/mk_pat_db.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+# -- /usr/bin/env python
 """
 Reads a pattern database and generates the corresponding
 header file.

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 8, 11, 0)
+    set_version(4, 8, 12, 0)
     
 # Z3 Project definition
 def init_project_def():

scripts/pyg2hpp.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#  - /usr/bin/env python
 """
 Reads a pyg file and emits the corresponding
 C++ header file into the specified destination

scripts/release.yml

@@ -72,6 +72,43 @@ stages:
         artifactName: 'UbuntuBuild'
         targetPath: $(Build.ArtifactStagingDirectory)
 
+
+  - job: UbuntuDoc
+    displayName: "Ubuntu Doc build"
+    pool:
+      vmImage: "Ubuntu-18.04"
+    steps:
+    - script: sudo apt-get install ocaml opam libgmp-dev
+    - script: sudo apt-get install doxygen
+    - script: sudo apt-get install graphviz
+    - script: opam init -y
+    - script: eval `opam config env`; opam install zarith ocamlfind -y
+    - script: python scripts/mk_make.py --ml --staticlib
+    - script: |
+        set -e
+        cd build
+        eval `opam config env` 
+        make -j3
+        make -j3 examples
+        make -j3 test-z3
+        ./ml_example
+        cd ..
+    - script: |
+        set -e
+        eval `opam config env` 
+        cd doc
+        python mk_api_doc.py --mld --z3py-package-path=../build/python/z3
+        mkdir api/html/ml
+        ocamldoc -html -d api/html/ml -sort -hide Z3 -I $( ocamlfind query zarith ) -I ../build/api/ml ../build/api/ml/z3enums.mli ../build/api/ml/z3.mli
+        cd ..
+    - script: zip -r z3doc.zip doc/api
+    - script: cp z3doc.zip $(Build.ArtifactStagingDirectory)/.
+    - task: PublishPipelineArtifact@0
+      inputs:
+        artifactName: 'UbuntuDoc'
+        targetPath: $(Build.ArtifactStagingDirectory)
+	
+
   - job: ManyLinuxBuild
     displayName: "ManyLinux build"
     pool:
@@ -283,6 +320,11 @@ stages:
       inputs:
         artifact: 'UbuntuBuild'
         path: $(Agent.TempDirectory)
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download Doc"
+      inputs:
+        artifact: 'UbuntuDoc'
+        path: $(Agent.TempDirectory)
     - task: DownloadPipelineArtifact@2
       displayName: 'Download macOS Build'
       inputs:
@@ -323,9 +365,9 @@ stages:
         isDraft: true
         isPreRelease: false
 
-  # Enable on release:
+  # Enable on release (after fixing Nuget key)
   - job: NuGetPublish
-    condition: eq(0,1)
+    condition: eq(1,0)
     displayName: "Publish to NuGet.org"
     steps:
     - task: DownloadPipelineArtifact@2
@@ -346,7 +388,7 @@ stages:
 
   # Enable on release:
   - job: PyPIPublish
-    condition: eq(0,1)
+    condition: eq(1,1)
     displayName: "Publish to PyPI"
     pool:
       vmImage: "ubuntu-latest"

scripts/update_api.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#  - !/usr/bin/env python
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
 #

src/api/java/Optimize.java

@@ -73,6 +73,28 @@ public class Optimize extends Z3Object {
         Assert(constraints);
     }
 
+    /** 
+     * Assert a constraint into the optimizer, and track it (in the unsat) core
+     * using the Boolean constant p. 
+     * 
+     * Remarks: 
+     * This API is an alternative to {@link #check} with assumptions for
+     * extracting unsat cores.
+     * Both APIs can be used in the same solver. The unsat core will contain a
+     * combination
+     * of the Boolean variables provided using {@link #assertAndTrack}
+     * and the Boolean literals
+     * provided using {@link #check} with assumptions.
+     */ 
+    public void AssertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
+    {
+        getContext().checkContextMatch(constraint);
+        getContext().checkContextMatch(p);
+
+        Native.optimizeAssertAndTrack(getContext().nCtx(), getNativeObject(),
+                constraint.getNativeObject(), p.getNativeObject());
+    }
+
     /**
      * Handle to objectives returned by objective functions.
      **/

src/api/ml/z3.ml

@@ -1272,7 +1272,7 @@ struct
   let mk_re_concat ctx args = Z3native.mk_re_concat ctx (List.length args) args
   let mk_re_range = Z3native.mk_re_range
   let mk_re_loop = Z3native.mk_re_loop
-  let mk_re_intersect = Z3native.mk_re_intersect
+  let mk_re_intersect ctx args = Z3native.mk_re_intersect ctx (List.length args) args
   let mk_re_complement = Z3native.mk_re_complement
   let mk_re_empty = Z3native.mk_re_empty
   let mk_re_full = Z3native.mk_re_full

src/api/ml/z3.mli

@@ -1850,115 +1850,115 @@ end
 (** Sequences, Strings and Regular Expressions **)
 module Seq : 
 sig
-  (* create a sequence sort *)
+  (** create a sequence sort *)
   val mk_seq_sort : context -> Sort.sort -> Sort.sort
 
-  (* test if sort is a sequence sort *)
+  (** test if sort is a sequence sort *)
   val is_seq_sort : context -> Sort.sort -> bool
 
-  (* create regular expression sorts over sequences of the argument sort *)   
+  (** create regular expression sorts over sequences of the argument sort *)   
   val mk_re_sort : context -> Sort.sort -> Sort.sort
 
-  (* test if sort is a regular expression sort *)
+  (** test if sort is a regular expression sort *)
   val is_re_sort : context -> Sort.sort -> bool
 
-  (* create string sort *)
+  (** create string sort *)
   val mk_string_sort : context -> Sort.sort
 
-  (* test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
+  (** test if sort is a string sort (a sequence of 8-bit bit-vectors) *)
   val is_string_sort : context -> Sort.sort -> bool 
 
-  (* create a string literal *)
+  (** create a string literal *)
   val mk_string : context -> string -> Expr.expr
 
-  (* test if expression is a string *)
+  (** test if expression is a string *)
   val is_string : context -> Expr.expr -> bool 
 
-  (* retrieve string from string Expr.expr *)
+  (** retrieve string from string Expr.expr *)
   val get_string : context -> Expr.expr -> string 
 
-  (* the empty sequence over base sort *)
+  (** the empty sequence over base sort *)
   val mk_seq_empty : context -> Sort.sort -> Expr.expr 
 
-  (* a unit sequence *)
+  (** a unit sequence *)
   val mk_seq_unit : context -> Expr.expr -> Expr.expr 
 
-  (* sequence concatenation *)
+  (** sequence concatenation *)
   val mk_seq_concat : context -> Expr.expr list -> Expr.expr 
 
-  (* predicate if the first argument is a prefix of the second *)
+  (** predicate if the first argument is a prefix of the second *)
   val mk_seq_prefix : context -> Expr.expr -> Expr.expr -> Expr.expr  
 
-  (* predicate if the first argument is a suffix of the second *)
+  (** predicate if the first argument is a suffix of the second *)
   val mk_seq_suffix : context -> Expr.expr -> Expr.expr -> Expr.expr  
 
-  (* predicate if the first argument contains the second *)
+  (** predicate if the first argument contains the second *)
   val mk_seq_contains : context -> Expr.expr -> Expr.expr -> Expr.expr  
 
-  (* extract sub-sequence starting at index given by second argument and of length provided by third argument *)
+  (** extract sub-sequence starting at index given by second argument and of length provided by third argument *)
   val mk_seq_extract : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr  
 
-  (* replace first occurrence of second argument by third *)
+  (** replace first occurrence of second argument by third *)
   val mk_seq_replace : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr  
 
-  (* a unit sequence at index provided by second argument *)
+  (** a unit sequence at index provided by second argument *)
   val mk_seq_at : context -> Expr.expr -> Expr.expr -> Expr.expr 
 
-  (* length of a sequence *)
+  (** length of a sequence *)
   val mk_seq_length : context -> Expr.expr -> Expr.expr  
 
-  (* index of the first occurrence of the second argument in the first *)
+  (** index of the first occurrence of the second argument in the first *)
   val mk_seq_index : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr 
 
-  (* retrieve integer expression encoded in string *)
+  (** retrieve integer expression encoded in string *)
   val mk_str_to_int : context -> Expr.expr -> Expr.expr
 
-  (* compare strings less-than-or-equal *)
+  (** compare strings less-than-or-equal *)
   val mk_str_le : context -> Expr.expr -> Expr.expr -> Expr.expr
 
-  (* compare strings less-than *)
+  (** compare strings less-than *)
   val mk_str_lt : context -> Expr.expr -> Expr.expr -> Expr.expr
 
-  (* convert an integer expression to a string *)
+  (** convert an integer expression to a string *)
   val mk_int_to_str : context -> Expr.expr -> Expr.expr 
 
-  (* create regular expression that accepts the argument sequence *)
+  (** create regular expression that accepts the argument sequence *)
   val mk_seq_to_re : context -> Expr.expr -> Expr.expr 
 
-  (* regular expression membership predicate *)
+  (** regular expression membership predicate *)
   val mk_seq_in_re : context -> Expr.expr -> Expr.expr -> Expr.expr 
 
-  (* regular expression plus *)
+  (** regular expression plus *)
   val mk_re_plus : context -> Expr.expr -> Expr.expr 
 
-  (* regular expression star *)
+  (** regular expression star *)
   val mk_re_star : context -> Expr.expr -> Expr.expr 
 
-  (* optional regular expression *)
+  (** optional regular expression *)
   val mk_re_option : context -> Expr.expr -> Expr.expr 
 
-  (* union of regular expressions *)
+  (** union of regular expressions *)
   val mk_re_union : context -> Expr.expr list -> Expr.expr 
 
-  (* concatenation of regular expressions *)
+  (** concatenation of regular expressions *)
   val mk_re_concat : context -> Expr.expr list -> Expr.expr 
   
-  (* regular expression for the range between two characters *)
+  (** regular expression for the range between two characters *)
   val mk_re_range : context -> Expr.expr -> Expr.expr -> Expr.expr 
 
-  (* bounded loop regular expression *)
+  (** bounded loop regular expression *)
   val mk_re_loop : context -> Expr.expr -> int -> int -> Expr.expr 
   
-  (* intersection of regular expressions *)
+  (** intersection of regular expressions *)
-  val mk_re_intersect : context -> int -> Expr.expr list -> Expr.expr
+  val mk_re_intersect : context -> Expr.expr list -> Expr.expr
 
-  (* the regular expression complement *)
+  (** the regular expression complement *)
   val mk_re_complement : context -> Expr.expr -> Expr.expr 
 
-  (* the regular expression that accepts no sequences *)
+  (** the regular expression that accepts no sequences *)
   val mk_re_empty : context -> Sort.sort -> Expr.expr 
 
-  (* the regular expression that accepts all sequences *)
+  (** the regular expression that accepts all sequences *)
   val mk_re_full : context -> Sort.sort -> Expr.expr 
 
 end

src/api/z3_api.h

@@ -4620,8 +4620,9 @@ extern "C" {
 
     /**
        \brief Return a hash code for the given AST.
-       The hash code is structural. You can use Z3_get_ast_id interchangeably with
+       The hash code is structural but two different AST objects can map to the same hash.
-       this function.
+       The result of \c Z3_get_ast_id returns an indentifier that is unique over the 
+       set of live AST objects.
 
        def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
     */

src/api/z3_fpa.h

@@ -961,7 +961,8 @@ extern "C" {
 
         \param c logical context
         \param t a floating-point numeral
-        \param sgn sign
+        \param sgn the retrieved sign
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
         NaN, which is an invalid argument.
@@ -975,6 +976,7 @@ extern "C" {
 
         \param c logical context
         \param t a floating-point numeral
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
         enough to represent the real significand precisely.
@@ -1004,6 +1006,7 @@ extern "C" {
         \param c logical context
         \param t a floating-point numeral
         \param biased flag to indicate whether the result is in biased representation
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: This function extracts the exponent in `t`, without normalization.
         NaN is an invalid argument.
@@ -1019,6 +1022,7 @@ extern "C" {
         \param t a floating-point numeral
         \param n exponent
         \param biased flag to indicate whether the result is in biased representation
+        \returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
 
         Remarks: This function extracts the exponent in `t`, without normalization.
         NaN is an invalid argument.

src/ast/ast.cpp

@@ -559,10 +559,11 @@ unsigned get_node_hash(ast const * n) {
             return to_sort(n)->get_name().hash();
         else
             return combine_hash(to_sort(n)->get_name().hash(), to_sort(n)->get_info()->hash());
-    case AST_FUNC_DECL:
+    case AST_FUNC_DECL: {
+        unsigned h = combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_range()->hash());
         return ast_array_hash(to_func_decl(n)->get_domain(), to_func_decl(n)->get_arity(),
-                              to_func_decl(n)->get_info() == nullptr ?
+            combine_hash(h, to_func_decl(n)->get_info() == nullptr ?  0 : to_func_decl(n)->get_info()->hash()));
-                              to_func_decl(n)->get_name().hash() : combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_info()->hash()));
+    }
     case AST_APP:
         return ast_array_hash(to_app(n)->get_args(),
                               to_app(n)->get_num_args(),

src/ast/euf/euf_egraph.cpp

@@ -745,7 +745,7 @@ namespace euf {
             out << "] ";
         }
         if (n->value() != l_undef) 
-            out << "[v" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
+            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
             for (auto v : enode_th_vars(n))

src/ast/euf/euf_etable.h

@@ -87,8 +87,8 @@ namespace euf {
             bool operator()(enode * n1, enode * n2) const {
                 SASSERT(n1->num_args() == 2);
                 SASSERT(n2->num_args() == 2);
-
+                if (n1->get_decl() != n2->get_decl())
-                SASSERT(n1->get_decl() == n2->get_decl());
+                    return false;
                 enode* c1_1 = get_root(n1, 0);  
                 enode* c1_2 = get_root(n1, 1); 
                 enode* c2_1 = get_root(n2, 0); 

src/ast/normal_forms/pull_quant.cpp

@@ -63,7 +63,7 @@ struct pull_quant::imp {
             
             for (unsigned i = 0; i < num_children; i++) {
                 expr * child = children[i];
-                if (is_quantifier(child)) {
+                if (is_quantifier(child) && !is_lambda(child)) {
                     
                     if (!found_quantifier && (is_forall(child) || is_exists(child))) {
                         found_quantifier = true;
@@ -184,11 +184,11 @@ struct pull_quant::imp {
             // Remark: patterns are ignored.
             // See comment in reduce1_app
             result = m.mk_forall(var_sorts.size(),
-                                         var_sorts.data(),
+				 var_sorts.data(),
-                                         var_names.data(),
+				 var_names.data(),
-                                         nested_q->get_expr(),
+				 nested_q->get_expr(),
-                                         std::min(q->get_weight(), nested_q->get_weight()),
+				 std::min(q->get_weight(), nested_q->get_weight()),
-                                         q->get_qid());
+				 m.is_lambda_def(q) ? symbol("pulled-lambda") : q->get_qid());
         }
 
         void pull_quant1(quantifier * q, expr * new_expr, expr_ref & result) {

src/ast/rewriter/seq_eq_solver.cpp

@@ -148,6 +148,7 @@ namespace seq {
         expr_ref_vector const* _es = nullptr;
         if (!match_itos3(e, n, _es))
             return false;
+
         expr_ref_vector const& es = *_es;
 
         if (es.empty()) {
@@ -183,6 +184,8 @@ namespace seq {
             expr_ref digit = m_ax.sk().mk_digit2int(u);
             add_consequence(m_ax.mk_ge(digit, 1));
         }
+	    expr_ref y(seq.str.mk_concat(e.rs, e.ls[0]->get_sort()), m);
+	    ctx.add_solution(e.ls[0], y);
         return true;
     }
 

src/ast/rewriter/seq_rewriter.cpp

@@ -1775,6 +1775,10 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         result = str().mk_concat(c, a);
         return BR_REWRITE1;
     }
+    if (str().is_empty(a) && str().is_empty(c)) {
+        result = a;
+        return BR_DONE;
+    }
 
     m_lhs.reset();
     str().get_concat(a, m_lhs);

src/ast/seq_decl_plugin.h

@@ -185,7 +185,7 @@ public:
 
     expr * get_some_value(sort * s) override;
 
-    bool is_char(ast* a) const { return a == m_char; }
+    bool is_char(sort* a) const { return a == m_char; }
 
     unsigned max_char() const { return get_char_plugin().max_char(); }
     unsigned num_bits() const { return get_char_plugin().num_bits(); }
@@ -222,7 +222,8 @@ public:
     sort* mk_string_sort() const { return seq.string_sort(); }
 
     bool is_char(sort* s) const { return seq.is_char(s); }
-    bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
+    bool is_char(expr* e) const { return is_char(e->get_sort()); }
+    bool is_string(sort* s) const { return is_seq(s) && seq.is_char(to_sort(s->get_parameter(0).get_ast())); }
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
     bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
     bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT)  && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
@@ -230,7 +231,6 @@ public:
     bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
     bool is_re(expr* e) const { return is_re(e->get_sort()); }
     bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); }
-    bool is_char(expr* e) const { return is_char(e->get_sort()); }
     bool is_const_char(expr* e, unsigned& c) const;
     bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); }
     bool is_char_le(expr const* e) const;

src/math/lp/nla_core.cpp

@@ -36,7 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_emons(m_evars),
     m_reslim(lim),
     m_use_nra_model(false),
-    m_nra(s, lim, *this)
+    m_nra(s, m_nra_lim, *this)
 {
     m_nlsat_delay = lp_settings().nlsat_delay();
 }
@@ -1563,10 +1563,15 @@ bool core::should_run_bounded_nlsat() {
 
 lbool core::bounded_nlsat() {
     params_ref p;
+    lbool ret;
     p.set_uint("max_conflicts", 100);
-    scoped_rlimit sr(m_reslim, 100000);
     m_nra.updt_params(p);
-    lbool ret = m_nra.check(); 
+    {
+        scoped_limits sl(m_reslim);
+        sl.push_child(&m_nra_lim);
+        scoped_rlimit sr(m_nra_lim, 100000);
+        ret = m_nra.check();
+    }
     p.set_uint("max_conflicts", UINT_MAX);           
     m_nra.updt_params(p);
     m_stats.m_nra_calls++;

src/math/lp/nla_core.h

@@ -175,6 +175,7 @@ private:
     svector<lpvar>           m_add_buffer;
     mutable lp::u_set        m_active_var_set;
     lp::u_set                m_rows;
+    reslimit                 m_nra_lim;
 public:
     reslimit&                m_reslim;
     bool                     m_use_nra_model;

src/math/polysat/log.cpp

@@ -1,5 +1,9 @@
 #ifndef _MSC_VER
 #include <unistd.h>  // for isatty
+#else
+#include <windows.h>
+#include <io.h>
+#undef min
 #endif
 #include <utility>
 
@@ -54,11 +58,11 @@ level_color(LogLevel msg_level)
 {
   switch (msg_level) {
     case LogLevel::Heading1:
-      return "\x1B[31m"; // red
+      return ""; // red
     case LogLevel::Heading2:
-      return "\x1B[33m"; // yellow
+      return ""; // yellow
     case LogLevel::Heading3:
-      return "\x1B[34m"; // blue
+      return ""; // blue
     default:
       return nullptr;
   }
@@ -70,16 +74,20 @@ std::pair<std::ostream&, bool>
 polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */)
 {
   std::ostream& os = std::cerr;
-#if 0
-  int const fd = fileno(stderr);
 
   size_t width = 20;
   size_t padding = width - std::min(width, fn.size());
-
-#ifdef _MSC_VER
   char const* color = nullptr;
+  color = level_color(msg_level);
+#ifdef _MSC_VER    
+  HANDLE hOut = GetStdHandle(STD_ERROR_HANDLE);
+  bool ok = hOut != INVALID_HANDLE_VALUE;
+  DWORD dwMode = 0;
+  ok = ok && GetConsoleMode(hOut, &dwMode);
+  dwMode |= ENABLE_VIRTUAL_TERMINAL_PROCESSING;
+  ok = ok && SetConsoleMode(hOut, dwMode);
 #else
-  char const* color = level_color(msg_level);
+  int const fd = _fileno(stderr);
   if (color && !isatty(fd)) { color = nullptr; }
 #endif
 
@@ -87,9 +95,6 @@ polysat_log(LogLevel msg_level, std::string fn, std::string /* pretty_fn */)
   os << "[" << fn << "] " << std::string(padding, ' ');
   os << std::string(polysat_log_indent_level, ' ');
   return {os, (bool)color};
-#else
-  return {os, false};
-#endif
 
 }
 

src/math/simplex/model_based_opt.cpp

@@ -134,20 +134,29 @@ namespace opt {
     }
 
     void model_based_opt::def::normalize() {
-        if (m_div.is_one()) return;
+        SASSERT(m_div.is_int());
+        if (m_div.is_neg()) {
+            for (var& v : m_vars)
+                v.m_coeff.neg();
+            m_coeff.neg();
+            m_div.neg();
+        }
+        if (m_div.is_one())
+            return;
         rational g(m_div);
+        if (!m_coeff.is_int())
+            return;
         g = gcd(g, m_coeff);
         for (var const& v : m_vars) {
+            if (!v.m_coeff.is_int())
+                return;
             g = gcd(g, abs(v.m_coeff));
-            if (g.is_one()) break;
+            if (g.is_one()) 
-        }
+                break;
-        if (m_div.is_neg()) {
-            g.neg();
         }
         if (!g.is_one()) {
-            for (var& v : m_vars) {
+            for (var& v : m_vars) 
                 v.m_coeff /= g;            
-            }
             m_coeff /= g;
             m_div /= g;
         }
@@ -1130,9 +1139,12 @@ namespace opt {
         }
         TRACE("opt1", display(tout << "tableau after replace x by y := v" << y << "\n"););
         def result = project(y, compute_def);
-        if (compute_def) 
+        if (compute_def) {
             result = (result * D) + u;
-        SASSERT(!compute_def || eval(result) == eval(x));
+            m_var2value[x] = eval(result);
+        }
+        TRACE("opt1", display(tout << "tableau after project y" << y << "\n"););
+	
         return result;
     }
 
@@ -1181,7 +1193,7 @@ namespace opt {
     // 3 | -t  & 21 | (-ct + 3s) & a-t <= 3u
 
     model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) {
-        TRACE("opt", tout << "v" << x << "\n" << m_rows[row_id1] << "\n";);
+        TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";);
         rational a = get_coefficient(row_id1, x), b;
         ineq_type ty = m_rows[row_id1].m_type;
         SASSERT(!a.is_zero());
@@ -1231,6 +1243,7 @@ namespace opt {
         if (compute_def) {
             result = def(m_rows[row_id1], x);
             m_var2value[x] = eval(result);
+            TRACE("opt1", tout << "updated eval " << x << " := " << eval(x) << "\n";);
         }
         retire_row(row_id1);
         return result;

src/model/func_interp.cpp

@@ -369,16 +369,14 @@ expr_ref func_interp::get_array_interp_core(func_decl * f) const {
     if (m_else == nullptr) 
         return r;
     ptr_vector<sort> domain;
-    for (sort* s : *f) {
+    for (sort* s : *f) 
         domain.push_back(s);    
-    }
 
     bool ground = is_ground(m_else);
     for (func_entry * curr : m_entries) {
         ground &= is_ground(curr->get_result());
-        for (unsigned i = 0; i < m_arity; i++) {
+        for (unsigned i = 0; i < m_arity; i++) 
             ground &= is_ground(curr->get_arg(i));        
-        }
     }
     if (!ground) {
         r = get_interp();

src/model/model.cpp

@@ -224,7 +224,7 @@ struct model::top_sort : public ::top_sort<func_decl> {
     }
 };
 
-void model::compress() {
+void model::compress(bool force_inline) {
     if (m_cleaned) return;
 
     // stratify m_finterp and m_decls in a topological sort
@@ -238,7 +238,7 @@ void model::compress() {
         collect_deps(ts);
         ts.topological_sort();
         for (func_decl * f : ts.top_sorted()) {
-            cleanup_interp(ts, f);
+            cleanup_interp(ts, f, force_inline);
         }
 
         func_decl_set removed;
@@ -332,11 +332,11 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
    \brief Inline interpretations of skolem functions
 */
 
-void model::cleanup_interp(top_sort& ts, func_decl* f) {
+void model::cleanup_interp(top_sort& ts, func_decl* f, bool force_inline) {
     unsigned pid = ts.partition_id(f);
     expr * e1 = get_const_interp(f);
     if (e1) {
-        expr_ref e2 = cleanup_expr(ts, e1, pid);
+        expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
         if (e2 != e1) 
             register_decl(f, e2);
         return;
@@ -344,11 +344,11 @@ void model::cleanup_interp(top_sort& ts, func_decl* f) {
     func_interp* fi = get_func_interp(f);
     if (fi) {
         e1 = fi->get_else();
-        expr_ref e2 = cleanup_expr(ts, e1, pid);
+        expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
         if (e1 != e2) 
             fi->set_else(e2);
         for (auto& fe : *fi) {
-            e2 = cleanup_expr(ts, fe->get_result(), pid);
+            e2 = cleanup_expr(ts, fe->get_result(), pid, force_inline);
             if (e2 != fe->get_result()) {
                 fi->insert_entry(fe->get_args(), e2);
             }
@@ -382,21 +382,26 @@ void model::collect_occs(top_sort& ts, expr* e) {
     for_each_ast(collector, e, true);
 }
 
-bool model::can_inline_def(top_sort& ts, func_decl* f) {
+bool model::can_inline_def(top_sort& ts, func_decl* f, bool force_inline) {
     if (ts.occur_count(f) <= 1) return true;
     func_interp* fi = get_func_interp(f);
-    if (!fi) return false;
+    if (!fi) 
-    if (fi->get_else() == nullptr) return false;
+        return false;
-    if (m_inline) return true;
+    if (fi->get_else() == nullptr) 
+        return false;
+    if (m_inline) 
+        return true;
     expr* e = fi->get_else();
     obj_hashtable<expr> subs;
     ptr_buffer<expr> todo;
     todo.push_back(e);
     while (!todo.empty()) {
-        if (fi->num_entries() + subs.size() > 8) return false;
+        if (!force_inline && fi->num_entries() + subs.size() > 8) 
+            return false;
         expr* e = todo.back();
         todo.pop_back();
-        if (subs.contains(e)) continue;
+        if (subs.contains(e)) 
+            continue;
         subs.insert(e);
         if (is_app(e)) {
             for (expr* arg : *to_app(e)) {
@@ -411,7 +416,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) {
 }
 
 
-expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) {
+expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline) {
     if (!e) return expr_ref(nullptr, m);
 
     TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";);
@@ -455,7 +460,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             if (autil.is_as_array(a)) {
                 func_decl* f = autil.get_as_array_func_decl(a);
                 // only expand auxiliary definitions that occur once.
-                if (can_inline_def(ts, f)) {
+                if (can_inline_def(ts, f, force_inline)) {
                     fi = get_func_interp(f);
                     if (fi) {
                         new_t = fi->get_array_interp(f);
@@ -467,7 +472,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             if (new_t) {
                 // noop
             }
-            else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && 
+            else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) && 
                      fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
                 var_subst vs(m, false);
                 new_t = vs(fi->get_interp(), args.size(), args.data());
@@ -526,15 +531,15 @@ expr_ref model::unfold_as_array(expr* e) {
 }
 
 
-expr_ref model::get_inlined_const_interp(func_decl* f) {
+expr_ref model::get_inlined_const_interp(func_decl* f, bool force_inline) {
     expr* v = get_const_interp(f);
     if (!v) return expr_ref(nullptr, m);
     top_sort st(m);
     expr_ref result1(v, m);
-    expr_ref result2 = cleanup_expr(st, v, UINT_MAX);
+    expr_ref result2 = cleanup_expr(st, v, UINT_MAX, force_inline);
     while (result1 != result2) {
         result1 = result2;
-        result2 = cleanup_expr(st, result1, UINT_MAX);
+        result2 = cleanup_expr(st, result1, UINT_MAX, force_inline);
     }
     return result2;
 }

src/model/model.h

@@ -50,10 +50,10 @@ protected:
     void collect_deps(top_sort& ts);    
     void collect_occs(top_sort& ts, func_decl* f);
     void collect_occs(top_sort& ts, expr* e);
-    void cleanup_interp(top_sort& ts, func_decl * f);
+    void cleanup_interp(top_sort& ts, func_decl * f, bool force_inline);
-    expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition);
+    expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline);
     void remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s);
-    bool can_inline_def(top_sort& ts, func_decl* f);
+    bool can_inline_def(top_sort& ts, func_decl* f, bool force_inline);
     value_factory* get_factory(sort* s);
 
 public:
@@ -78,7 +78,7 @@ public:
     sort * get_uninterpreted_sort(unsigned idx) const override;
     bool has_uninterpreted_sort(sort * s) const;
 
-    expr_ref get_inlined_const_interp(func_decl* f);
+    expr_ref get_inlined_const_interp(func_decl* f, bool force_inline);
     expr_ref unfold_as_array(expr* e);
 
     //
@@ -90,7 +90,7 @@ public:
     //
     model * translate(ast_translation & translator) const;
 
-    void compress();
+    void compress(bool force_inline = false);
 
     void set_model_completion(bool f) { m_mev.set_model_completion(f); }
     void updt_params(params_ref const & p);

src/qe/mbp/mbp_arith.cpp

@@ -281,9 +281,10 @@ namespace mbp {
             obj_map<expr, unsigned> tids;
             expr_ref_vector pinned(m);
             unsigned j = 0;
-            TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";
+            TRACE("qe", tout << "vars: " << vars << "\n";
                   for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";);
-            for (expr* fml : fmls) {
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                expr* fml = fmls.get(i);
                 if (!linearize(mbo, eval, fml, fmls, tids)) {
                     TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";);
                     fmls[j++] = fml;
@@ -293,7 +294,9 @@ namespace mbp {
                 }
             }
             fmls.shrink(j);
-            TRACE("qe", tout << "formulas\n" << fmls << "\n";);
+            TRACE("qe", tout << "formulas\n" << fmls << "\n";
+		                for (auto [e, id] : tids)
+		                    tout << mk_pp(e, m) << " -> " << id << "\n";);
 
             // fmls holds residue,
             // mbo holds linear inequalities that are in scope

src/qe/mbp/mbp_plugin.cpp

@@ -102,7 +102,7 @@ namespace mbp {
         model_evaluator eval(model);
         eval.set_expand_array_equalities(true);
         TRACE("qe", tout << fmls << "\n";);
-        DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n";); SASSERT(!m.is_false(eval(fml))); });
+        DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
 
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;

src/sat/sat_local_search.h

@@ -187,7 +187,7 @@ namespace sat {
 
         unsigned num_constraints() const { return m_constraints.size(); } // constraint index from 1 to num_constraint
 
-        uint64_t constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; }
+        int64_t constraint_slack(unsigned ci) const { return m_constraints[ci].m_slack; }
 
         void init();
         void reinit();

src/sat/smt/arith_diagnostics.cpp

@@ -50,7 +50,7 @@ namespace arith {
                     scoped_anum an(m_nla->am());
                     m_nla->am().display(out << " = ", nl_value(v, an));
                 }
-                else if (can_get_value(v))  
+                else if (can_get_value(v) && !m_solver->has_changed_columns())  
                     out << " = " << get_value(v);
                 if (is_int(v)) 
                     out << ", int";

src/sat/smt/arith_solver.h

@@ -384,7 +384,7 @@ namespace arith {
 
         obj_map<expr, expr*>      m_predicate2term;
         obj_map<expr, bound_info> m_term2bound_info;
-        bool                      m_model_is_initialized{ false };
+        bool                      m_model_is_initialized = false;
 
         unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
         bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; }

src/sat/smt/euf_internalize.cpp

@@ -139,6 +139,10 @@ namespace euf {
             sat::literal lit2 = literal(v, false);
             s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
+            if (relevancy_enabled()) {
+                add_aux(~lit, lit2);
+                add_aux(lit, ~lit2);
+            }
             lit = lit2;
         }
 
@@ -278,6 +282,7 @@ namespace euf {
             }
             else {
                 sat::bool_var v = si.to_bool_var(c);
+                s().set_external(v);
                 VERIFY(v != sat::null_bool_var);
                 VERIFY(s().is_external(v));
                 SASSERT(v != sat::null_bool_var);

src/sat/smt/euf_solver.cpp

@@ -302,13 +302,17 @@ namespace euf {
         size_t* c = to_ptr(l);
         SASSERT(is_literal(c));
         SASSERT(l == get_literal(c));
-        if (!sign && n->is_equality()) {
+	    if (n->value_conflict()) {
+            euf::enode* nb = sign ? mk_false() : mk_true();
+            m_egraph.merge(n, nb, c);
+	    }
+        else if (!sign && n->is_equality()) {
             SASSERT(!m.is_iff(e));
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, c);
         }
-        else if (n->merge_tf() || n->value_conflict()) {
+        else if (n->merge_tf()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }

src/sat/smt/euf_solver.h

@@ -352,6 +352,7 @@ namespace euf {
         sat::literal attach_lit(sat::literal lit, expr* e);
         void unhandled_function(func_decl* f);
         th_rewriter& get_rewriter() { return m_rewriter; }
+        void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
 
         // relevancy

src/sat/smt/q_clause.cpp

@@ -32,6 +32,12 @@ namespace q {
                 << mk_bounded_pp(rhs, m, 2);
     }
 
+    std::ostream& binding::display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const {
+        for (unsigned i = 0; i < num_nodes; ++i) 
+            out << ctx.bpp((*this)[i]) << " ";
+        return out;
+    }
+
     std::ostream& clause::display(euf::solver& ctx, std::ostream& out) const {
         out << "clause:\n";
         for (auto const& lit : m_lits)
@@ -39,9 +45,7 @@ namespace q {
         binding* b = m_bindings;
         if (b) {
             do {
-                for (unsigned i = 0; i < num_decls(); ++i)
+                b->display(ctx, num_decls(), out) << "\n";
-                    out << ctx.bpp((*b)[i]) << " ";
-                out << "\n";            
                 b = b->next();
             }
             while (b != m_bindings);

src/sat/smt/q_clause.h

@@ -49,6 +49,8 @@ namespace q {
         euf::enode* const* nodes() { return m_nodes; }
 
         euf::enode* operator[](unsigned i) const { return m_nodes[i]; }
+
+        std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const;
     };
 
     struct clause {

src/sat/smt/q_ematch.cpp

@@ -192,20 +192,26 @@ namespace q {
     }
 
     struct ematch::remove_binding : public trail {
+        euf::solver& ctx;
         clause& c;
         binding* b;
-        remove_binding(clause& c, binding* b): c(c), b(b) {}
+        remove_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {}
         void undo() override {            
+            SASSERT(binding::contains(c.m_bindings, b));
             binding::remove_from(c.m_bindings, b);
+            binding::detach(b);
         }        
     };
 
     struct ematch::insert_binding : public trail {
+        euf::solver& ctx;
         clause& c;
         binding* b;
-        insert_binding(clause& c, binding* b): c(c), b(b) {}
+        insert_binding(euf::solver& ctx, clause& c, binding* b): ctx(ctx), c(c), b(b) {}
         void undo() override {            
+            SASSERT(!c.m_bindings || c.m_bindings->invariant());
             binding::push_to_front(c.m_bindings, b);
+            SASSERT(!c.m_bindings || c.m_bindings->invariant());
         }
     };
 
@@ -230,7 +236,7 @@ namespace q {
         for (unsigned i = 0; i < n; ++i)
             b->m_nodes[i] = _binding[i];        
         binding::push_to_front(c.m_bindings, b);
-        ctx.push(remove_binding(c, b));
+        ctx.push(remove_binding(ctx, c, b));
     }
 
     void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@@ -395,7 +401,12 @@ namespace q {
         for (expr* arg : ors) {
             bool sign = m.is_not(arg, arg);
             expr* l, *r;
-            if (!m.is_eq(arg, l, r) || is_ground(arg)) {
+            if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
+                l = to_app(arg)->get_arg(0);
+                r = to_app(arg)->get_arg(1);
+                sign = !sign;
+            }
+            else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
                 l = arg;
                 r = sign ? m.mk_false() : m.mk_true();
                 sign = false;
@@ -503,8 +514,10 @@ namespace q {
             while (b != c.m_bindings);
 
             for (auto* b : to_remove) {
+                SASSERT(binding::contains(c.m_bindings, b));
                 binding::remove_from(c.m_bindings, b);
-                ctx.push(insert_binding(c, b));
+                binding::detach(b);
+                ctx.push(insert_binding(ctx, c, b));
             }
             to_remove.reset();
         }

src/sat/smt/q_mbi.cpp

@@ -213,6 +213,7 @@ namespace q {
         sat::literal qlit = ctx.expr2literal(q);
         if (is_exists(q))
             qlit.neg();
+        ctx.rewrite(proj);
         TRACE("q", tout << "project: " << proj << "\n";);
         ++m_stats.m_num_instantiations;        
         unsigned generation = ctx.get_max_generation(proj);    

src/sat/smt/q_solver.cpp

@@ -41,7 +41,7 @@ namespace q {
         quantifier* q = to_quantifier(e);
 
         auto const& exp = expand(q);
-        if (exp.size() > 1 && is_forall(q)) {
+        if (exp.size() > 1 && is_forall(q) && !l.sign()) {
             for (expr* e : exp) {
                 sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
                 add_clause(~l, lit);                    
@@ -50,14 +50,13 @@ namespace q {
             }
             return;
         }
-        if (exp.size() > 1 && is_exists(q)) {
+        if (exp.size() > 1 && is_exists(q) && l.sign()) {
             sat::literal_vector lits;
             lits.push_back(~l);
             for (expr* e : exp)
                 lits.push_back(ctx.internalize(e, l.sign(), false, false));
             add_clause(lits);
-            if (ctx.relevancy_enabled())
+            ctx.add_root(lits);
-                ctx.add_root(lits);
             return;
         }
 

src/smt/qi_queue.cpp

@@ -387,7 +387,7 @@ namespace smt {
             bool result = true;
             for (unsigned i = 0; i < sz; i++) {
                 entry & e       = m_delayed_entries[i];
-                TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
+                TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << " min-cost: " << min_cost << ", instantiated: " << e.m_instantiated << "\n";);
                 if (!e.m_instantiated && e.m_cost <= min_cost) {
                     TRACE("qi_queue",
                           tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";);

src/smt/smt_context_pp.cpp

@@ -608,14 +608,14 @@ namespace smt {
             clause * cls = j.get_clause();
             out << "clause ";
             if (cls) out << literal_vector(cls->get_num_literals(), cls->begin());
-            if (cls) display_literals_smt2(out << "\n", cls->get_num_literals(), cls->begin());
+            // if (cls) display_literals_smt2(out << "\n", cls->get_num_literals(), cls->begin());
             break;
         }
         case b_justification::JUSTIFICATION: {
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
-            display_literals_smt2(out, lits);
+            // display_literals_smt2(out, lits);
             break;
         }
         default:

src/smt/smt_model_checker.cpp

@@ -218,7 +218,7 @@ namespace smt {
             TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
 
             if (use_inv) {
-                unsigned sk_term_gen;
+	            unsigned sk_term_gen = 0;
                 expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
                 if (sk_term != nullptr) {
                     TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);

src/smt/smt_theory.cpp

@@ -195,6 +195,18 @@ namespace smt {
         log_axiom_instantiation(mk_or(fmls));
     }
 
+
+    void theory::log_axiom_instantiation(literal_buffer const& ls) {
+        ast_manager& m = get_manager();
+        expr_ref_vector fmls(m);
+        expr_ref tmp(m);
+        for (literal l : ls) {
+            ctx.literal2expr(l, tmp);
+            fmls.push_back(tmp);
+        }
+        log_axiom_instantiation(mk_or(fmls));
+    }
+
     void theory::log_axiom_instantiation(app * r, unsigned axiom_id, unsigned num_bindings, app * const * bindings, unsigned pattern_id, const vector<std::tuple<enode *, enode *>> & used_enodes) {
         ast_manager & m = get_manager();
         app_ref _r(r, m);

src/smt/smt_theory.h

@@ -124,6 +124,12 @@ namespace smt {
                 }
             }
 
+            scoped_trace_stream(theory& th, literal_buffer const& lits) : m(th.get_manager()) {
+                if (m.has_trace_stream()) {
+                    th.log_axiom_instantiation(lits);
+                }
+            }
+
             scoped_trace_stream(theory& th, literal lit): m(th.get_manager()) {
                 if (m.has_trace_stream()) {
                     literal_vector lits;
@@ -464,6 +470,8 @@ namespace smt {
 
         void log_axiom_instantiation(literal_vector const& ls);
 
+        void log_axiom_instantiation(literal_buffer const& ls);
+
         void log_axiom_instantiation(app * r, unsigned num_blamed_enodes, enode ** blamed_enodes) {
             vector<std::tuple<enode *, enode *>> used_enodes;
             for (unsigned i = 0; i < num_blamed_enodes; ++i) {

src/smt/theory_bv.cpp

@@ -646,9 +646,8 @@ namespace smt {
               );
        
         ctx.mark_as_relevant(l);
-        if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
+        scoped_trace_stream _ts(*this, l);
         ctx.mk_th_axiom(get_id(), 1, &l);
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
     }
 
     void theory_bv::internalize_int2bv(app* n) {    
@@ -688,9 +687,10 @@ namespace smt {
 
         literal l(mk_eq(lhs, rhs, false));
         ctx.mark_as_relevant(l);
-        if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
+        {
-        ctx.mk_th_axiom(get_id(), 1, &l);
+            scoped_trace_stream _ts(*this, l);
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+            ctx.mk_th_axiom(get_id(), 1, &l);
+        }
         
         TRACE("bv", 
               tout << mk_pp(lhs, m) << " == \n";
@@ -704,17 +704,29 @@ namespace smt {
         for (unsigned i = 0; i < sz; ++i) {
             numeral div = power(numeral(2), i);
             mod = numeral(2);
-            rhs = (i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_numeral(div, true));
+            expr_ref div_rhs((i == 0) ? e : m_autil.mk_idiv(e, m_autil.mk_numeral(div, true)), m);
-            rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true));
+            rhs = m_autil.mk_mod(div_rhs, m_autil.mk_numeral(mod, true));
             rhs = ctx.mk_eq_atom(rhs, m_autil.mk_int(1));
             lhs = n_bits.get(i);
             TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
             l = literal(mk_eq(lhs, rhs, false));
             ctx.mark_as_relevant(l);
-            if (m.has_trace_stream()) log_axiom_instantiation(ctx.bool_var2expr(l.var()));
+            {
-            ctx.mk_th_axiom(get_id(), 1, &l);
+                scoped_trace_stream _st(*this, l);
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+                ctx.mk_th_axiom(get_id(), 1, &l);
-            
+            }
+            {
+                // 0 < e < 2^i => e div 2^i = 0                
+                expr_ref zero(m_autil.mk_int(0), m);
+                literal a = mk_literal(m_autil.mk_ge(e, m_autil.mk_int(div)));
+                literal b = mk_literal(m_autil.mk_ge(e, zero));
+                literal c = mk_eq(div_rhs, zero, false);
+                ctx.mark_as_relevant(a);
+                ctx.mark_as_relevant(b);
+                ctx.mark_as_relevant(c);
+                // scoped_trace_stream _st(*this, a, ~b);
+                ctx.mk_th_axiom(get_id(), a, ~b, c);
+            }
         }
     }
 

src/smt/theory_lra.cpp

@@ -1170,14 +1170,11 @@ public:
         VERIFY(a.is_is_int(n, x));
         literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
         literal is_int = ctx().get_literal(n);
-        if (m.has_trace_stream()) {
+        scoped_trace_stream _sts1(th, ~is_int, eq);
-            app_ref body(m);
+        scoped_trace_stream _sts2(th, is_int, ~eq);
-            body = m.mk_iff(n, ctx().bool_var2expr(eq.var()));
-            th.log_axiom_instantiation(body);
-        }
         mk_axiom(~is_int, eq);
         mk_axiom(is_int, ~eq);
-        if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+
     }
 
     // create axiom for 
@@ -1248,6 +1245,7 @@ public:
             mk_axiom(eq);
             mk_axiom(mk_literal(a.mk_ge(mod, zero)));
             mk_axiom(mk_literal(a.mk_le(mod, upper)));
+            
             {
                 std::function<void(void)> log = [&,this]() {
                     th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
@@ -1320,13 +1318,8 @@ public:
                 exprs.push_back(c.bool_var2expr(mod_j.var()));
                 ctx().mark_as_relevant(mod_j);
             }
-            if (m.has_trace_stream()) {
+            scoped_trace_stream _st(th, lits);
-                app_ref body(m);
-                body = m.mk_or(exprs.size(), exprs.data());
-                th.log_axiom_instantiation(body);
-            }
             ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());                
-            if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
         }            
     }
 
@@ -1749,20 +1742,14 @@ public:
                 literal p_ge_r1  = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
                 literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
                 literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
-                if (m.has_trace_stream()) {
+                {
-                    app_ref body(m);
+                    scoped_trace_stream _sts(th, ~p_le_r1, n_le_div);
-                    body = m.mk_implies(ctx().bool_var2expr(p_le_r1.var()), ctx().bool_var2expr(n_le_div.var()));
+                    mk_axiom(~p_le_r1, n_le_div);
-                    th.log_axiom_instantiation(body);
                 }
-                mk_axiom(~p_le_r1, n_le_div); 
+                {
-                if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
+                    scoped_trace_stream _sts(th, ~p_ge_r1, n_ge_div);
-                if (m.has_trace_stream()) {
+                    mk_axiom(~p_ge_r1, n_ge_div);
-                    app_ref body(m);
-                    body = m.mk_implies(ctx().bool_var2expr(p_ge_r1.var()), ctx().bool_var2expr(n_ge_div.var()));
-                    th.log_axiom_instantiation(body);
                 }
-                mk_axiom(~p_ge_r1, n_ge_div);
-                if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
 
                 all_divs_valid = false;
 

src/smt/theory_recfun.cpp

@@ -288,6 +288,8 @@ namespace smt {
         scoped_trace_stream _tr(*this, fn);
         ctx.mk_th_axiom(get_id(), 1, &lit);
         TRACEFN("macro expansion yields " << pp_lit(ctx, lit));
+	    if (has_quantifiers(rhs))
+	        throw default_exception("quantified formulas in recursive functions are not supported");
     }
 
     /**
@@ -392,6 +394,8 @@ namespace smt {
         std::function<literal_vector(void)> fn = [&]() { return clause; };
         scoped_trace_stream _tr(*this, fn);
         ctx.mk_th_axiom(get_id(), clause);
+        if (has_quantifiers(rhs))
+            throw default_exception("quantified formulas in recursive functions are not supported");
     }
     
     final_check_status theory_recfun::final_check_eh() {

src/smt/theory_seq.cpp

@@ -403,7 +403,10 @@ final_check_status theory_seq::final_check_eh() {
         TRACEFIN("branch_ne");
         return FC_CONTINUE;
     }    
-
+    if (branch_itos()) {
+        TRACEFIN("branch_itos");
+        return FC_CONTINUE;
+    }
     if (m_unhandled_expr) {
         TRACEFIN("give_up");
         TRACE("seq", tout << "unhandled: " << mk_pp(m_unhandled_expr, m) << "\n";);
@@ -1544,9 +1547,50 @@ bool theory_seq::check_int_string(expr* e) {
         return true;
     if (m_util.str.is_stoi(e, n) && !m_util.str.is_itos(n) && add_length_to_eqc(n))
         return true;
+
     return false;
 }
 
+bool theory_seq::branch_itos() {
+    bool change = false;
+    for (expr * e : m_int_string) {
+        if (branch_itos(e))
+            change = true;
+    }
+    return change;
+}
+
+bool theory_seq::branch_itos(expr* e) {
+    expr* n = nullptr;
+    rational val;
+    if (ctx.inconsistent())
+        return true;
+    if (!m_util.str.is_itos(e, n))
+        return false;
+    if (!ctx.e_internalized(e))
+        return false;
+    enode* r = ctx.get_enode(e)->get_root();
+    if (m_util.str.is_string(r->get_expr()))
+        return false;
+    if (!get_num_value(n, val))
+        return false;
+    if (val.is_neg())
+        return false;    
+    literal b = mk_eq(e, m_util.str.mk_string(val.to_string()), false);
+    if (ctx.get_assignment(b) == l_true)
+        return false;
+    if (ctx.get_assignment(b) == l_false) {
+        literal a = mk_eq(n, m_autil.mk_int(val), false);
+        add_axiom(~a, b);
+    }
+    else {
+        ctx.force_phase(b);
+        ctx.mark_as_relevant(b);
+    }
+    return true;
+}
+
+
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
     mk_var(n);

src/smt/theory_seq.h

@@ -566,6 +566,8 @@ namespace smt {
         void add_int_string(expr* e);
         bool check_int_string();
         bool check_int_string(expr* e);
+        bool branch_itos();
+        bool branch_itos(expr* e);
 
         expr_ref add_elim_string_axiom(expr* n);
         void add_in_re_axiom(expr* n);

src/util/dlist.h

@@ -74,6 +74,10 @@ public:
         }
     }
 
+    static void detach(T* elem) {
+        elem->init(elem);
+    }
+
     bool invariant() const {
         auto* e = this;
         do {
@@ -84,6 +88,20 @@ public:
         while (e != this);
         return true;
     }
+
+
+    static bool contains(T* list, T* elem) {
+        if (!list)
+            return false;
+        T* first = list;
+        do {
+            if (list == elem)
+                return true;
+            list = list->m_next;
+        }         
+        while (list != first);
+        return false;
+    }
 };