Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

doc/mk_api_doc.py

@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation 2015
+
 import os
 import shutil
 import re

examples/c++/example.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<vector>
 #include"z3++.h"
 

examples/c/test_capi.c

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<stdio.h>
 #include<stdlib.h>
 #include<stdarg.h>

examples/interp/iz3.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <iostream>

examples/maxsat/maxsat.c

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /*
   Simple MAXSAT solver on top of the Z3 API.
 */

examples/python/example.py

@@ -1,3 +1,5 @@
+# Copyright (c) Microsoft Corporation 2015
+
 from z3 import *
 
 x = Real('x')

examples/tptp/tptp5.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include <string>
 #include <cstring>
 #include <list>

examples/tptp/tptp5.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef TPTP5_H_
 #define TPTP5_H_
 

examples/tptp/tptp5.lex.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #line 2 "tptp5.lex.cpp"
 
 #line 4 "tptp5.lex.cpp"

scripts/mk_copyright.py

@@ -0,0 +1,57 @@
+# Copyright (c) 2015 Microsoft Corporation
+
+import os
+import re
+
+cr = re.compile("Copyright")
+aut = re.compile("Automatically generated")
+
+cr_notice = """
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+"""
+
+def has_cr(file):
+    ins = open(file)
+    lines = 0
+    line = ins.readline()
+    while line and lines < 20:
+	m = cr.search(line)
+	if m:
+	    ins.close()
+	    return True
+	m = aut.search(line)
+	if m:
+	    ins.close()
+	    return True
+	line = ins.readline()
+    ins.close()
+    return False
+
+def add_cr(file):
+    tmp = "%s.tmp" % file
+    ins = open(file)
+    ous = open(tmp,'w')
+    ous.write(cr_notice)
+    line = ins.readline()
+    while line:
+	ous.write(line)
+	line = ins.readline()
+    ins.close()
+    ous.close()
+    os.system("move %s %s" % (tmp, file))
+    
+def add_missing_cr(dir):
+    for root, dirs, files in os.walk(dir):
+	for f in files:
+	    if f.endswith('.cpp') or f.endswith('.h') or f.endswith('.c'):
+		path = "%s\\%s" % (root, f)
+		if not has_cr(path):
+		    print "Missing CR for %s" % path
+		    add_cr(path)
+
+add_missing_cr('src')
+add_missing_cr('examples')

scripts/trackall.sh

@@ -1,7 +1,9 @@
 #!/bin/bash
 
+# Copyright (c) 2015 Microsoft Corporation
 # Script for "cloning" (and tracking) all branches at codeplex.
 # On Windows, this script must be executed in the "git Bash" console.
+
 for branch in `git branch -a | grep remotes | grep -v HEAD | grep -v master`; do
     git branch --track ${branch##*/} $branch
 done

src/api/api_context.cpp

@@ -516,6 +516,11 @@ extern "C" {
         memory::initialize(0);
     }
 
+    void Z3_API Z3_finalize_memory(void) {
+        LOG_Z3_finalize_memory();
+        memory::finalize();
+    }
+
     Z3_error_code Z3_API Z3_get_error_code(Z3_context c) {
         LOG_Z3_get_error_code(c);
         return mk_c(c)->get_error_code();

src/api/api_fpa.cpp

@@ -712,7 +712,7 @@ extern "C" {
 
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s) {
         Z3_TRY;
-        LOG_Z3_fpa_get_ebits(c, s);
+        LOG_Z3_fpa_get_sbits(c, s);
         RESET_ERROR_CODE();
         CHECK_NON_NULL(s, 0);
         return mk_c(c)->fpautil().get_sbits(to_sort(s));
@@ -765,7 +765,30 @@ extern "C" {
         mpqm.display_decimal(ss, q, sbits);
         return mk_c(c)->mk_external_string(ss.str());
         Z3_CATCH_RETURN("");
+    }
 
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
+        Z3_TRY;
+        LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
+        fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
+        scoped_mpf val(mpfm);
+        bool r = plugin->is_numeral(to_expr(t), val);
+        if (!r) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        const mpz & z = mpfm.sig(val);
+        if (!mpzm.is_uint64(z)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        *n = mpzm.get_uint64(z);
+        return 1;
+        Z3_CATCH_RETURN(0);
     }
 
     Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
@@ -794,7 +817,7 @@ extern "C" {
 
     Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
         Z3_TRY;
-        LOG_Z3_fpa_get_numeral_exponent_string(c, t);
+        LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         mpf_manager & mpfm = mk_c(c)->fpautil().fm();

src/api/dll/dll.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 
 #include<windows.h>

src/api/dotnet/FPNum.cs

@@ -59,6 +59,25 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The significand value of a floating-point numeral as a UInt64
+        /// </summary>
+        /// <remarks>
+        /// This function extracts the significand bits, without the 
+        /// hidden bit or normalization. Throws an exception if the
+        /// significand does not fit into a UInt64.
+        /// </remarks>
+        public UInt64 SignificandUInt64
+        {
+            get
+            {
+                UInt64 result = 0;
+                if (Native.Z3_fpa_get_numeral_significand_uint64(Context.nCtx, NativeObject, ref result) == 0)
+                    throw new Z3Exception("Significand is not a 64 bit unsigned integer");                
+                return result;
+            }
+        }
+
         /// <summary>
         /// Return the exponent value of a floating-point numeral as a string
         /// </summary>

src/api/dotnet/Goal.cs

@@ -208,6 +208,21 @@ namespace Microsoft.Z3
             return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Goal to BoolExpr conversion.
+        /// </summary>
+        /// <returns>A string representation of the Goal.</returns>
+        public BoolExpr AsBoolExpr() {
+            uint n = Size;
+            if (n == 0) 
+                return Context.MkTrue();
+            else if (n == 1)                
+                return Formulas[0];
+            else {
+                return Context.MkAnd(Formulas);
+            }
+        }
+
         #region Internal
         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 

src/api/java/FPNum.java

@@ -43,6 +43,21 @@ public class FPNum extends FPExpr
         return Native.fpaGetNumeralSignificandString(getContext().nCtx(), getNativeObject());
     }
 
+    /**
+     * The significand value of a floating-point numeral as a UInt64
+     * Remarks: This function extracts the significand bits, without the 
+     * hidden bit or normalization. Throws an exception if the
+     * significand does not fit into a UInt64.
+     * @throws Z3Exception
+     **/
+    public long getSignificandUInt64()
+    {
+        Native.LongPtr res = new Native.LongPtr();
+        if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true)
+            throw new Z3Exception("Significand is not a 64 bit unsigned integer");
+        return res.value;
+    }
+    
     /**
      * Return the exponent value of a floating-point numeral as a string
      * @throws Z3Exception 

src/api/java/FPSort.java

@@ -43,7 +43,7 @@ public class FPSort extends Sort
      * The number of significand bits.
      */
     public int getSBits() {
-        return Native.fpaGetEbits(getContext().nCtx(), getNativeObject());        
+        return Native.fpaGetSbits(getContext().nCtx(), getNativeObject());        
     }
     
 }

src/api/java/Goal.java

@@ -221,6 +221,22 @@ public class Goal extends Z3Object
             return "Z3Exception: " + e.getMessage();
         }
     }
+    
+    /** 
+     * Goal to BoolExpr conversion.
+     *  
+     * Returns a string representation of the Goal.
+     **/
+    public BoolExpr AsBoolExpr() {
+        int n = size();
+        if (n == 0) 
+            return getContext().mkTrue();
+        else if (n == 1)                
+            return getFormulas()[0];
+        else {
+            return getContext().mkAnd(getFormulas());
+        }
+    }
 
     Goal(Context ctx, long obj)
     {

src/api/ml/z3.ml

@@ -2059,6 +2059,8 @@ struct
 	(Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t))
   let get_numeral_significand_string ( ctx : context ) ( t : expr ) =
 	(Z3native.fpa_get_numeral_significand_string (context_gno ctx) (Expr.gno t))
+  let get_numeral_significand_uint ( ctx : context ) ( t : expr ) =
+	(Z3native.fpa_get_numeral_significand_uint64 (context_gno ctx) (Expr.gno t))
   let get_numeral_exponent_string ( ctx : context ) ( t : expr ) =
 	(Z3native.fpa_get_numeral_exponent_string (context_gno ctx) (Expr.gno t))
   let get_numeral_exponent_int ( ctx : context ) ( t : expr ) =
@@ -2197,6 +2199,15 @@ struct
     create ctx (Z3native.mk_goal (context_gno ctx) models unsat_cores proofs)
 
   let to_string ( x : goal ) = Z3native.goal_to_string (z3obj_gnc x) (z3obj_gno x)
+
+  let as_expr ( x : goal ) = 
+	let n = get_size x in
+	if n = 0 then 
+	  (Boolean.mk_true (z3obj_gc x)) 
+	else if n = 1 then
+	  (List.hd (get_formulas x))
+	else
+	  (Boolean.mk_and (z3obj_gc x) (get_formulas x))
 end  
 
 

src/api/ml/z3.mli

@@ -2161,6 +2161,12 @@ sig
   (** Return the significand value of a floating-point numeral as a string. *)
   val get_numeral_significand_string : context -> Expr.expr -> string
 
+  (** Return the significand value of a floating-point numeral as a uint64. 
+	  Remark: This function extracts the significand bits, without the 
+      hidden bit or normalization. Throws an exception if the
+      significand does not fit into a uint64. *)
+  val get_numeral_significand_uint : context -> Expr.expr -> bool * int
+
   (** Return the exponent value of a floating-point numeral as a string *)
   val get_numeral_exponent_string : context -> Expr.expr -> string
 
@@ -2647,6 +2653,9 @@ sig
 
   (**  A string representation of the Goal. *)
   val to_string : goal -> string
+
+  (** Goal to BoolExpr conversion. *)
+  val as_expr : goal -> Expr.expr
 end
 
 (** Models

src/api/ml/z3_stubs.c

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /* File generated from z3.idl */
 
 #include <stddef.h>

src/api/z3_api.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef _Z3_API_H_
 #define _Z3_API_H_
 
@@ -5365,7 +5371,19 @@ END_MLAPI_EXCLUDE
     */
     void Z3_API Z3_reset_memory(void);
 #endif
-    
+
+#ifdef CorML3
+    /**
+       \brief Destroy all allocated resources.
+
+       Any pointers previously returned by the API become invalid.
+       Can be used for memory leak detection.
+
+       def_API('Z3_finalize_memory', VOID, ())
+    */
+    void Z3_API Z3_finalize_memory(void);
+#endif
+
     /*@}*/
 
 #ifdef CorML3
@@ -6933,7 +6951,7 @@ END_MLAPI_EXCLUDE
 
        def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS)))
     */
-    Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
+    Z3_apply_result Z3_API Z3_tactic_apply_ex(__in Z3_context c, __in Z3_tactic t, __in Z3_goal g, __in Z3_params p);
 
 #ifdef CorML3
     /**

src/api/z3_fpa.h

@@ -858,6 +858,20 @@ extern "C" {
     */
     Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
 
+    /**
+        \brief Return the significand value of a floating-point numeral as a uint64.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        Remarks: This function extracts the significand bits in `t`, without the 
+        hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the 
+        significand does not fit into a uint64.
+
+        def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
+    */
+    Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
+
     /**
         \brief Return the exponent value of a floating-point numeral as a string
 

src/api/z3_macros.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifndef __in
 #define __in
 #endif

src/ast/fpa/fpa2bv_converter.cpp

@@ -1767,11 +1767,19 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
     m_simp.mk_ite(c52, v52, res_sig, res_sig);
     m_simp.mk_ite(c51, v51, res_sig, res_sig);
     res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0.
-    res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), m_bv_util.mk_extract(ebits+1, 0, shift));
+    
+    SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
+    SASSERT(m_bv_util.get_bv_size(shift) == sbits + 1);
+
+    expr_ref e_shift(m);
+    e_shift = (ebits + 2 <= sbits + 1) ? m_bv_util.mk_extract(ebits + 1, 0, shift) :
+                                         m_bv_util.mk_sign_extend((ebits + 2) - (sbits + 1), shift);
+    SASSERT(m_bv_util.get_bv_size(e_shift) == ebits + 2);
+    res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
 
     SASSERT(m_bv_util.get_bv_size(res_sgn) == 1);
-    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits+4);
+    SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
-    SASSERT(m_bv_util.get_bv_size(res_exp) == ebits+2);
+    SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
 
     // CMW: We use the rounder for normalization.
     round(f->get_range(), rm, res_sgn, res_sig, res_exp, v6); 

src/ast/proof_checker/proof_checker.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "proof_checker.h"
 #include "ast_ll_pp.h"
 #include "ast_pp.h"

src/ast/rewriter/expr_safe_replace.cpp

@@ -49,17 +49,23 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             app* c = to_app(a);
             unsigned n = c->get_num_args();
             m_args.reset();
+            bool arg_differs = false;
             for (unsigned i = 0; i < n; ++i) {
                 if (m_cache.find(c->get_arg(i), d)) {
                     m_args.push_back(d);
+                    arg_differs |= c->get_arg(i) != d;
                 }
                 else {
                     m_todo.push_back(c->get_arg(i));
                 }
             }
             if (m_args.size() == n) {
-                b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                if (arg_differs) {
-                m_refs.push_back(b);
+                    b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr());
+                    m_refs.push_back(b);
+                } else {
+                    b = a;
+                }
                 m_cache.insert(a, b);
                 m_todo.pop_back();
             }

src/ast/simplifier/bv_elim.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "bv_elim.h"
 #include "bv_decl_plugin.h"
 #include "var_subst.h"

src/muz/base/dl_boogie_proof.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /**
 
 Example from Boogie:

src/muz/base/dl_boogie_proof.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /**
 
 output     :: derivation model

src/muz/base/hnf.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 /*--
  Module Name:
  

src/muz/base/proof_utils.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "dl_util.h"
 #include "proof_utils.h"
 #include "ast_smt2_pp.h"

src/muz/fp/datalog_parser.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include"datalog_parser.h"
 #include"string_buffer.h"
 #include"str_hashtable.h"

src/muz/rel/check_relation.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "check_relation.h"
 #include "dl_relation_manager.h"
 #include "qe_util.h"

src/muz/rel/karr_relation.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "karr_relation.h"
 #include "bool_rewriter.h"
 

src/parsers/smt/smtlib.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include"smtlib.h"
 #include"ast_pp.h"
 #include"ast_smt2_pp.h"

src/qe/nlarith_util.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "ast.h"
 #include "nlarith_util.h"
 #include "arith_decl_plugin.h"

src/qe/qe_arith.h

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #ifndef __QE_ARITH_H_
 #define __QE_ARITH_H_
 

src/qe/qe_array_plugin.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include "qe.h"
 #include "array_decl_plugin.h"
 #include "expr_safe_replace.h"

src/qe/qe_cmd.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "qe_cmd.h"
 #include "qe.h"
 #include "cmd_context.h"

src/qe/qe_datatype_plugin.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 // ---------------------
 // datatypes
 // Quantifier elimination routine for recursive data-types.

src/qe/qe_dl_plugin.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include "qe.h"
 #include "expr_safe_replace.h"
 #include "dl_decl_plugin.h"

src/qe/qe_util.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "qe_util.h"
 #include "bool_rewriter.h"
 

src/shell/opt_frontend.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<fstream>
 #include<signal.h>
 #include<time.h>

src/shell/options.h

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 /**
    \page cmdline Command line options
    

src/smt/database.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 static char const g_pattern_database[] =
 "(benchmark patterns \n"
 " :status unknown \n"

src/smt/theory_arith.h

@@ -885,6 +885,7 @@ namespace smt {
         void add_tmp_row_entry(row & r, numeral const & coeff, theory_var v);
         enum max_min_t { UNBOUNDED, AT_BOUND, OPTIMIZED, BEST_EFFORT};
         max_min_t max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared);
+        bool has_interface_equality(theory_var v);
         bool max_min(svector<theory_var> const & vars);
 
         max_min_t max_min(row& r, bool max, bool maintain_integrality, bool& has_shared);

src/smt/theory_arith_aux.h

@@ -1545,6 +1545,25 @@ namespace smt {
         return is_tighter;
     }
 
+    /**
+       \brief Check if bound change affects interface equality.
+    */
+    template<typename Ext>
+    bool theory_arith<Ext>::has_interface_equality(theory_var x) {
+        theory_var num = get_num_vars();
+        context& ctx = get_context();
+        enode* r = get_enode(x)->get_root();
+        for (theory_var v = 0; v < num; v++) {
+            if (v == x) continue;
+            enode* n = get_enode(v);
+            if (ctx.is_shared(n) && n->get_root() == r) {
+                return true;
+            }
+        }
+        return false;
+    }
+    
+
     /**
        \brief Maximize (Minimize) the given temporary row.
        Return true if succeeded.
@@ -1660,13 +1679,23 @@ namespace smt {
                     SASSERT(!maintain_integrality || valid_assignment());
                     continue;
                 }
-                if (ctx.is_shared(get_enode(x_j))) {
+#if 0
+                if (ctx.is_shared(get_enode(x_j)) && has_interface_equality(x_j)) {
                     ++best_efforts;
                 }
                 else {
                     SASSERT(unbounded_gain(max_gain));
+                    has_shared = false;
                     best_efforts = 0;
                 }
+#endif
+                //
+                // NB. As it stands this is a possibly unsound conclusion for shared theories.
+                // the tradeoff is non-termination for unbounded objectives in the
+                // presence of sharing.
+                // 
+                has_shared = false;
+                best_efforts = 0;
                 result = UNBOUNDED;
                 break;
             }

src/tactic/arith/arith_bounds_tactic.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 
 #include"arith_bounds_tactic.h"
 #include"arith_decl_plugin.h"

src/tactic/arith/card2bv_tactic.cpp

@@ -485,7 +485,6 @@ public:
             return;
         }
                 
-        unsigned size = g->size();
         expr_ref new_f1(m), new_f2(m);
         proof_ref new_pr1(m), new_pr2(m);
         for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {

src/tactic/arith/pb2bv_tactic.cpp

@@ -854,7 +854,7 @@ private:
             m_temporary_ints(m),
             m_used_dependencies(m),
             m_rw(*this) {
-            updt_params(p);
+            updt_params(p);            
             m_b_rw.set_flat(false); // no flattening otherwise will blowup the memory
             m_b_rw.set_elim_and(true);
         }
@@ -871,12 +871,17 @@ private:
             m_max_memory   = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
             m_all_clauses_limit = p.get_uint("pb2bv_all_clauses_limit", 8);
             m_cardinality_limit = p.get_uint("pb2bv_cardinality_limit", UINT_MAX);
+            m_b_rw.updt_params(p);
         }
 
         void collect_param_descrs(param_descrs & r) {
-            insert_max_memory(r);
+            insert_max_memory(r);            
             r.insert("pb2bv_all_clauses_limit", CPK_UINT, "(default: 8) maximum number of literals for using equivalent CNF encoding of PB constraint.");
             r.insert("pb2bv_cardinality_limit", CPK_UINT, "(default: inf) limit for using arc-consistent cardinality constraint encoding.");
+
+            m_b_rw.get_param_descrs(r);        
+            r.erase("flat"); 
+            r.erase("elim_and");            
         }
         
         void set_cancel(bool f) {

src/tactic/smtlogics/qflia_tactic.cpp

@@ -56,7 +56,7 @@ struct quasi_pb_probe : public probe {
     }
 };
 
-probe * mk_quasi_pb_probe() {
+probe * mk_is_quasi_pb_probe() {
     return mk_and(mk_not(mk_is_unbounded_probe()),
                   alloc(quasi_pb_probe));
 }
@@ -100,9 +100,11 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
 #define SMALL_SIZE 80000
 
 static tactic * mk_pb_tactic(ast_manager & m) {
-    params_ref pb2bv_p;
+    params_ref pb2bv_p;    
-    pb2bv_p.set_bool("ite_extra", true);    
     pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
+
+    params_ref bv2sat_p;
+    bv2sat_p.set_bool("ite_extra", true);
     
     return and_then(fail_if_not(mk_is_pb_probe()),
                     fail_if(mk_produce_proofs_probe()),
@@ -113,14 +115,16 @@ static tactic * mk_pb_tactic(ast_manager & m) {
                                      mk_fail_if_undecided_tactic()),
                             and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
                                      fail_if_not(mk_is_qfbv_probe()),
-                                     mk_bv2sat_tactic(m))));
+                                     using_params(mk_bv2sat_tactic(m), bv2sat_p))));
 }
 
 
 static tactic * mk_lia2sat_tactic(ast_manager & m) {
     params_ref pb2bv_p;
-    pb2bv_p.set_bool("ite_extra", true);    
     pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
+
+    params_ref bv2sat_p;
+    bv2sat_p.set_bool("ite_extra", true);
     
     return and_then(fail_if(mk_is_unbounded_probe()),
                     fail_if(mk_produce_proofs_probe()),
@@ -130,7 +134,7 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
                     mk_lia2pb_tactic(m),
                     using_params(mk_pb2bv_tactic(m), pb2bv_p),
                     fail_if_not(mk_is_qfbv_probe()),                    
-                    mk_bv2sat_tactic(m));
+                    using_params(mk_bv2sat_tactic(m), bv2sat_p));
 }
 
 // Try to find a model for an unbounded ILP problem.
@@ -208,7 +212,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(preamble_st,
                                         or_else(mk_ilp_model_finder_tactic(m),
                                                 mk_pb_tactic(m),
-                                                and_then(fail_if_not(mk_quasi_pb_probe()), 
+                                                and_then(fail_if_not(mk_is_quasi_pb_probe()), 
                                                          using_params(mk_lia2sat_tactic(m), quasi_pb_p),
                                                          mk_fail_if_undecided_tactic()),
                                                 mk_bounded_tactic(m),

src/tactic/smtlogics/qflia_tactic.h

@@ -28,4 +28,11 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p = params_ref());
   ADD_TACTIC("qflia", "builtin strategy for solving QF_LIA problems.", "mk_qflia_tactic(m, p)")
 */
 
+
+probe * mk_is_quasi_pb_probe();
+
+/*
+  ADD_PROBE("is-quasi-pb", "true if the goal is quasi-pb.", "mk_is_quasi_pb_probe()")
+*/
+
 #endif

src/test/api.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "z3.h"
 #include "z3_private.h"

src/test/api_bug.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<stdio.h>
 #include"z3.h"
 

src/test/arith_rewriter.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "arith_rewriter.h"
 #include "bv_decl_plugin.h"
 #include "ast_pp.h"

src/test/arith_simplifier_plugin.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "arith_eq_solver.h"
 #include "smt_params.h"
 

src/test/bits.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 // Test some bit hacks
 #include"util.h"
 #include"debug.h"

src/test/bv_simplifier_plugin.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "bv_simplifier_plugin.h"
 #include "arith_decl_plugin.h"
 #include "ast_pp.h"

src/test/check_assumptions.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "memory_manager.h"
 #include "smt_params.h"
 #include "ast.h"

src/test/datalog_parser.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "datalog_parser.h"
 #include "ast_pp.h"
 #include "arith_decl_plugin.h"

src/test/ddnf.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "ddnf.h"
 #include "tbv.h"
 #include <iostream>

src/test/dl_context.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "datalog_parser.h"
 #include "ast_pp.h"
 #include "arith_decl_plugin.h"

src/test/dl_product_relation.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "dl_context.h"
 #include "dl_register_engine.h"

src/test/dl_query.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "datalog_parser.h"
 #include "ast_pp.h"
 #include "dl_table_relation.h"

src/test/dl_relation.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "dl_context.h"
 #include "dl_register_engine.h"

src/test/dl_table.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "dl_context.h"
 #include "dl_table.h"

src/test/dl_util.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "dl_util.h"
 
 using namespace datalog;

src/test/doc.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "doc.h"
 #include "trace.h"
 #include "vector.h"

src/test/expr_rand.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "expr_rand.h"
 #include "ast_pp.h"
 #include "bv_decl_plugin.h"

src/test/expr_substitution.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "expr_substitution.h"
 #include "smt_params.h"
 #include "substitution.h"

src/test/factor_rewriter.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "factor_rewriter.h"
 #include "bv_decl_plugin.h"
 #include "ast_pp.h"

src/test/fuzzing/expr_delta.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "expr_delta.h"
 #include "ast_pp.h"
 

src/test/fuzzing/expr_rand.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "expr_rand.h"
 #include "bv_decl_plugin.h"
 #include "array_decl_plugin.h"

src/test/get_implied_equalities.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "z3.h"
 #include "trace.h"
 #include "debug.h"

src/test/heap_trie.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "heap_trie.h"
 
 struct unsigned_le {

src/test/hilbert_basis.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "hilbert_basis.h"
 #include "ast_pp.h"
 #include "reg_decl_plugins.h"

src/test/horn_subsume_model_converter.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include "horn_subsume_model_converter.h"
 #include "arith_decl_plugin.h"
 #include "model_smt2_pp.h"

src/test/karr.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "hilbert_basis.h"
 
 /*

src/test/memory.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "z3.h"
 #include "z3_private.h"

src/test/model2expr.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "model2expr.h"
 #include "ast_pp.h"
 #include "arith_decl_plugin.h"

src/test/model_retrieval.cpp

@@ -1,4 +1,10 @@
 
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
+
 #include "ast.h"
 #include "smt_params.h"
 #include "smt_context.h"

src/test/nlarith_util.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "nlarith_util.h"
 #include "arith_decl_plugin.h"
 #include "ast_pp.h"

src/test/pdr.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "pdr_context.h"
 #include "reg_decl_plugins.h"
 

src/test/polynorm.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "th_rewriter.h"
 #include "smt2parser.h"
 #include "arith_decl_plugin.h"

src/test/proof_checker.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "proof_checker.h"
 #include "ast_ll_pp.h"
 

src/test/qe_arith.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "qe_arith.h"
 #include "qe.h"
 #include "th_rewriter.h"

src/test/quant_elim.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "ast.h"
 #include "smt_params.h"
 #include "simplifier.h"

src/test/quant_solve.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "ast.h"
 #include "smt_params.h"
 #include "qe.h"

src/test/sat_user_scope.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "sat_solver.h"
 #include "util.h"
 

src/test/simplex.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "sparse_matrix.h"
 #include "sparse_matrix_def.h"
 #include "simplex.h"

src/test/simplifier.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #ifdef _WINDOWS
 #include "z3.h"
 #include "z3_private.h"

src/test/small_object_allocator.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include<iostream>
 #include"util.h"
 #include"trace.h"

src/test/smt2print_parse.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 // This is to test the print-parse facilities over the API
 // for SMT-LIB2.
 

src/test/smt_context.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "smt_context.h"
 #include "reg_decl_plugins.h"
 

src/test/sorting_network.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "trace.h"
 #include "vector.h"
 #include "ast.h"

src/test/substitution.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "expr_substitution.h"
 #include "smt_params.h"
 #include "substitution.h"

src/test/tbv.cpp

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #include "tbv.h"
 
 static void tst1(unsigned num_bits) {

src/test/test_util.h

@@ -1,3 +1,9 @@
+
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+--*/
+
 #pragma once
 
 #include "stopwatch.h"