Merge branch 'master' of https://github.com/z3prover/z3

CMakeLists.txt

@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 6)
-set(Z3_VERSION_PATCH 1)
+set(Z3_VERSION_PATCH 2)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
@@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
   message(STATUS "Platform: FreeBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
+  message(STATUS "Platform: NetBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
   message(STATUS "Platform: OpenBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
@@ -409,6 +412,20 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
 ################################################################################
 include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
 
+################################################################################
+# If using Ninja, force color output for Clang (and gcc, disabled to check build).
+################################################################################
+if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
+  endif()
+#  if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+#    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
+#    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
+#  endif()
+endif()
+
 ################################################################################
 # Option to control what type of library we build
 ################################################################################
@@ -434,7 +451,7 @@ else()
 endif()
 
 ################################################################################
-# Postion independent code
+# Position independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add

configure

@@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /dev/null ; then
    exit 1
 fi
 
-$PYTHON scripts/mk_make.py $*
+$PYTHON scripts/mk_make.py "$@"

examples/tptp/tptp5.cpp

@@ -1609,7 +1609,6 @@ public:
                 display_inference(out, "rewrite", "thm", p);
                 break;
             case Z3_OP_PR_PULL_QUANT: 
-            case Z3_OP_PR_PULL_QUANT_STAR: 
                 display_inference(out, "pull_quant", "thm", p);
                 break;
             case Z3_OP_PR_PUSH_QUANT: 
@@ -1669,12 +1668,6 @@ public:
             case Z3_OP_PR_NNF_NEG: 
                 display_inference(out, "nnf_neg", "sab", p); 
                 break;
-            case Z3_OP_PR_NNF_STAR: 
-                display_inference(out, "nnf", "sab", p); 
-                break;
-            case Z3_OP_PR_CNF_STAR: 
-                display_inference(out, "cnf", "sab", p); 
-                break;
             case Z3_OP_PR_SKOLEMIZE:
                 display_inference(out, "skolemize", "sab", p); 
                 break;                
@@ -1706,10 +1699,6 @@ public:
             return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2);
         }
         case Z3_OP_PR_NNF_POS:
-        case Z3_OP_PR_NNF_STAR: 
-            return display_hyp_inference(out, "nnf", "sab", conclusion, hyp);
-        case Z3_OP_PR_CNF_STAR: 
-            return display_hyp_inference(out, "cnf", "sab", conclusion, hyp);
         case Z3_OP_PR_SKOLEMIZE:
             return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp);
         case Z3_OP_PR_TRANSITIVITY:

scripts/mk_consts_files.py

@@ -72,7 +72,7 @@ def main(args):
 
     if count == 0:
         logging.info('No files generated. You need to specific an output directory'
-                     ' for the relevant langauge bindings')
+                     ' for the relevant language bindings')
     # TODO: Add support for other bindings
     return 0
 

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 6, 1, 0)
+    set_version(4, 6, 2, 0)
     add_lib('util', [])
     add_lib('lp', ['util'], 'util/lp')
     add_lib('polynomial', ['util'], 'math/polynomial')

scripts/mk_util.py

@@ -69,6 +69,7 @@ IS_WINDOWS=False
 IS_LINUX=False
 IS_OSX=False
 IS_FREEBSD=False
+IS_NETBSD=False
 IS_OPENBSD=False
 IS_CYGWIN=False
 IS_CYGWIN_MINGW=False
@@ -141,6 +142,9 @@ def is_linux():
 def is_freebsd():
     return IS_FREEBSD
 
+def is_netbsd():
+    return IS_NETBSD
+
 def is_openbsd():
     return IS_OPENBSD
 
@@ -604,6 +608,8 @@ elif os.name == 'posix':
         IS_LINUX=True
     elif os.uname()[0] == 'FreeBSD':
         IS_FREEBSD=True
+    elif os.uname()[0] == 'NetBSD':
+        IS_NETBSD=True
     elif os.uname()[0] == 'OpenBSD':
         IS_OPENBSD=True
     elif os.uname()[0][:6] == 'CYGWIN':
@@ -889,8 +895,13 @@ def is_CXX_gpp():
     return is_compiler(CXX, 'g++')
 
 def is_clang_in_gpp_form(cc):
-    version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8')
+    str = check_output([cc, '--version'])
-    return version_string.find('clang') != -1
+    try:
+       version_string = str.encode('utf-8')
+    except:
+       version_string = str
+    clang = 'clang'.encode('utf-8')
+    return version_string.find(clang) != -1
 
 def is_CXX_clangpp():
     if is_compiler(CXX, 'g++'):
@@ -1240,7 +1251,7 @@ def get_so_ext():
     sysname = os.uname()[0]
     if sysname == 'Darwin':
         return 'dylib'
-    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
+    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
         return 'so'
     elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
         return 'dll'
@@ -1790,6 +1801,8 @@ class JavaDLLComponent(Component):
                 t = t.replace('PLATFORM', 'linux')
             elif IS_FREEBSD:
                 t = t.replace('PLATFORM', 'freebsd')
+            elif IS_NETBSD:
+                t = t.replace('PLATFORM', 'netbsd')
             elif IS_OPENBSD:
                 t = t.replace('PLATFORM', 'openbsd')
             elif IS_CYGWIN:
@@ -2499,6 +2512,13 @@ def mk_config():
             LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+        elif sysname == 'NetBSD':
+            CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
+            OS_DEFINES     = '-D_NETBSD_'
+            SO_EXT         = '.so'
+            LDFLAGS        = '%s -lrt' % LDFLAGS
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'OpenBSD':
             CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_OPENBSD_'

src/api/api_ast.cpp

@@ -919,7 +919,6 @@ extern "C" {
             case PR_REWRITE: return Z3_OP_PR_REWRITE;
             case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
             case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
-            case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
             case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
             case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
             case PR_DER: return Z3_OP_PR_DER;
@@ -936,9 +935,7 @@ extern "C" {
             case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
             case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
             case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
-            case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
             case PR_SKOLEMIZE:  return Z3_OP_PR_SKOLEMIZE;
-            case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
             case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
             case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
             case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;

src/api/c++/z3++.h

@@ -989,7 +989,7 @@ namespace z3 {
 
         /**
            \brief sequence and regular expression operations.
-           + is overloaeded as sequence concatenation and regular expression union.
+           + is overloaded as sequence concatenation and regular expression union.
            concat is overloaded to handle sequences and regular expressions
         */
         expr extract(expr const& offset, expr const& length) const { 

src/api/dotnet/Context.cs

@@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
 
 
         /// <summary>
-        /// Concatentate sequences.
+        /// Concatenate sequences.
         /// </summary>
         public SeqExpr MkConcat(params SeqExpr[] t)
         {
@@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+        /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
         /// or trivially unsatisfiable (i.e., contains `false').
         /// </summary>
         public Tactic FailIfNotDecided()
@@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a bit-vector.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
         /// the result will be rounded according to rounding mode rm.
         /// </remarks>
@@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a real-numbered term.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// real number. Note that this type of conversion will often result in non-linear
         /// constraints over real terms.
         /// </remarks>
@@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
         /// <remarks>
         /// The size of the resulting bit-vector is automatically determined. Note that
         /// IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        /// knows only one NaN and it will always produce the same bit-vector represenatation of
+        /// knows only one NaN and it will always produce the same bit-vector representation of
         /// that NaN.
         /// </remarks>
         /// <param name="t">FloatingPoint term.</param>

src/api/dotnet/Expr.cs

@@ -932,7 +932,7 @@ namespace Microsoft.Z3
         /// Indicates whether the term is a proof by condensed transitivity of a relation
         /// </summary>
         /// <remarks>
-        /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+        /// Condensed transitivity proof. 
         /// It combines several symmetry and transitivity proofs.
         /// Example:
         /// T1: (R a b)
@@ -1035,14 +1035,11 @@ namespace Microsoft.Z3
         /// </summary>
         /// <remarks>
         /// A proof for rewriting an expression t into an expression s.
-        /// This proof object is used if the parameter PROOF_MODE is 1.
         /// This proof object can have n antecedents.
         /// The antecedents are proofs for equalities used as substitution rules.
-        /// The object is also used in a few cases if the parameter PROOF_MODE is 2.
+        /// The object is used in a few cases:
-        /// The cases are:
         /// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
         /// - When converting bit-vectors to Booleans (BIT2BOOL=true)
-        /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
         /// </remarks>
         public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
 
@@ -1054,15 +1051,6 @@ namespace Microsoft.Z3
         /// </remarks>
         public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
 
-        /// <summary>
-        /// Indicates whether the term is a proof for pulling quantifiers out.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (iff P Q) where Q is in prenex normal form.
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        /// This proof object has no antecedents
-        /// </remarks>
-        public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
 
         /// <summary>
         /// Indicates whether the term is a proof for pushing quantifiers in.
@@ -1304,28 +1292,6 @@ namespace Microsoft.Z3
         /// </remarks>
         public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
 
-        /// <summary>
-        /// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (~ P Q) where Q is in negation normal form.
-        ///
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        ///
-        /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-        /// </remarks>
-        public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
-
-        /// <summary>
-        /// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (~ P Q) where Q is in conjunctive normal form.
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-        /// </remarks>
-        public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
-
         /// <summary>
         /// Indicates whether the term is a proof for a Skolemization step
         /// </summary>

src/api/java/Context.java

@@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
     }
     
     /**
-     * Concatentate sequences.
+     * Concatenate sequences.
      */
     public SeqExpr mkConcat(SeqExpr... t)
     {
@@ -2782,7 +2782,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Create a tactic that fails if the goal is not triviall satisfiable (i.e.,
+     * Create a tactic that fails if the goal is not trivially satisfiable (i.e.,
      * empty) or trivially unsatisfiable (i.e., contains `false').
      **/
     public Tactic failIfNotDecided()
@@ -3770,7 +3770,7 @@ public class Context implements AutoCloseable {
      * @param sz Size of the resulting bit-vector.
      * @param signed Indicates whether the result is a signed or unsigned bit-vector.
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
      * the result will be rounded according to rounding mode rm.        
      * @throws Z3Exception 
@@ -3787,7 +3787,7 @@ public class Context implements AutoCloseable {
      * Conversion of a floating-point term into a real-numbered term.
      * @param t FloatingPoint term
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * real number. Note that this type of conversion will often result in non-linear 
      * constraints over real terms.
      * @throws Z3Exception 
@@ -3803,7 +3803,7 @@ public class Context implements AutoCloseable {
      * Remarks:
      * The size of the resulting bit-vector is automatically determined. Note that 
      * IEEE 754-2008 allows multiple different representations of NaN. This conversion 
-     * knows only one NaN and it will always produce the same bit-vector represenatation of 
+     * knows only one NaN and it will always produce the same bit-vector representation of
      * that NaN. 
      * @throws Z3Exception 
      **/

src/api/java/Expr.java

@@ -1398,8 +1398,7 @@ public class Expr extends AST
     /**
      * Indicates whether the term is a proof by condensed transitivity of a
      * relation
-     * Remarks:  Condensed transitivity proof. This proof object is
+     * Remarks:  Condensed transitivity proof. It combines several symmetry
-     * only used if the parameter PROOF_MODE is 1. It combines several symmetry
      * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
      * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
      * 
@@ -1506,14 +1505,11 @@ public class Expr extends AST
     /**
      * Indicates whether the term is a proof by rewriting
      * Remarks:  A proof for
-     * rewriting an expression t into an expression s. This proof object is used
+     * rewriting an expression t into an expression s. This proof object can have n
-     * if the parameter PROOF_MODE is 1. This proof object can have n
      * antecedents. The antecedents are proofs for equalities used as
-     * substitution rules. The object is also used in a few cases if the
+     * substitution rules. The object is used in a few cases . The cases are: - When applying contextual
-     * parameter PROOF_MODE is 2. The cases are: - When applying contextual
      * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
-     * Booleans (BIT2BOOL=true) - When pulling ite expression up
+     * Booleans (BIT2BOOL=true) 
-     * (PULL_CHEAP_ITE_TREES=true) 
      * @throws Z3Exception on error
      * @return a boolean
      **/
@@ -1534,17 +1530,6 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
     }
 
-    /**
-     * Indicates whether the term is a proof for pulling quantifiers out.
-     * 
-     * Remarks:  A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofPullQuantStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
-    }
 
     /**
      * Indicates whether the term is a proof for pushing quantifiers in.
@@ -1804,38 +1789,6 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
     }
 
-    /**
-     * Indicates whether the term is a proof for (~ P Q) here Q is in negation
-     * normal form.
-     * Remarks:  A proof for (~ P Q) where Q is in negation normal
-     * form.
-     * 
-     * This proof object is only used if the parameter PROOF_MODE is 1.
-     * 
-     * This proof object may have n antecedents. Each antecedent is a
-     * PR_DEF_INTRO. 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofNNFStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
-    }
-
-    /**
-     * Indicates whether the term is a proof for (~ P Q) where Q is in
-     * conjunctive normal form.
-     * Remarks:  A proof for (~ P Q) where Q is in
-     * conjunctive normal form. This proof object is only used if the parameter
-     * PROOF_MODE is 1. This proof object may have n antecedents. Each
-     * antecedent is a PR_DEF_INTRO. 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofCNFStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
-    }
 
     /**
      * Indicates whether the term is a proof for a Skolemization step

src/api/ml/z3.ml

@@ -1402,7 +1402,6 @@ struct
   let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE)
   let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR)
   let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT)
-  let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR)
   let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT)
   let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS)
   let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER)
@@ -1419,8 +1418,6 @@ struct
   let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ)
   let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS)
   let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG)
-  let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR)
-  let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR)
   let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE)
   let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ)
   let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA)

src/api/python/z3/z3.py

@@ -2428,7 +2428,7 @@ def is_rational_value(a):
     return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
 
 def is_algebraic_value(a):
-    """Return `True` if `a` is an algerbraic value of sort Real.
+    """Return `True` if `a` is an algebraic value of sort Real.
 
     >>> is_algebraic_value(RealVal("3/5"))
     False
@@ -4437,7 +4437,7 @@ class Datatype:
         """Declare constructor named `name` with the given accessors `args`.
         Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
 
-        In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
+        In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
         declares the constructor named `cons` that builds a new List using an integer and a List.
         It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
         and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
@@ -4457,7 +4457,7 @@ class Datatype:
         return "Datatype(%s, %s)" % (self.name, self.constructors)
 
     def create(self):
-        """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
+        """Create a Z3 datatype based on the constructors declared using the method `declare()`.
 
         The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
 
@@ -8874,7 +8874,7 @@ class FPNumRef(FPRef):
     def isSubnormal(self):
         return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
 
-    """Indicates whether the numeral is postitive."""
+    """Indicates whether the numeral is positive."""
     def isPositive(self):
         return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
 
@@ -9670,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None):
     The size of the resulting bit-vector is automatically determined.
 
     Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-    knows only one NaN and it will always produce the same bit-vector represenatation of
+    knows only one NaN and it will always produce the same bit-vector representation of
     that NaN.
 
     >>> x = FP('x', FPSort(8, 24))
@@ -9845,7 +9845,7 @@ def Empty(s):
     raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
 
 def Full(s):
-    """Create the regular expression that accepts the universal langauge
+    """Create the regular expression that accepts the universal language
     >>> e = Full(ReSort(SeqSort(IntSort())))
     >>> print(e)
     re.all

src/api/z3.h

@@ -21,7 +21,8 @@ Notes:
 #ifndef Z3_H_
 #define Z3_H_
 
-#include<stdio.h>
+#include <stdio.h>
+#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"

src/api/z3_api.h

@@ -459,7 +459,7 @@ typedef enum
        [trans T1 T2]: (R t u)
        }
 
-   - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+   - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. 
      It combines several symmetry and transitivity proofs.
 
           Example:
@@ -539,21 +539,14 @@ typedef enum
           }
 
    - Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s.
-       This proof object is used if the parameter PROOF_MODE is 1.
        This proof object can have n antecedents.
        The antecedents are proofs for equalities used as substitution rules.
-       The object is also used in a few cases if the parameter PROOF_MODE is 2.
+       The proof rule is used in a few cases. The cases are:
-       The cases are:
          - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
          - When converting bit-vectors to Booleans (BIT2BOOL=true)
-         - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
 
    - Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
 
-   - Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form.
-       This proof object is only used if the parameter PROOF_MODE is 1.
-       This proof object has no antecedents.
-
    - Z3_OP_PR_PUSH_QUANT: A proof for:
 
        \nicebox{
@@ -726,15 +719,6 @@ typedef enum
          [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
                                    (and (or r_1 r_2) (or r_1' r_2')))
        }
-   - Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form.
-
-       This proof object is only used if the parameter PROOF_MODE is 1.
-
-       This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-
-   - Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form.
-       This proof object is only used if the parameter PROOF_MODE is 1.
-       This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
 
    - Z3_OP_PR_SKOLEMIZE: Proof for:
 
@@ -1142,7 +1126,6 @@ typedef enum {
     Z3_OP_PR_REWRITE,
     Z3_OP_PR_REWRITE_STAR,
     Z3_OP_PR_PULL_QUANT,
-    Z3_OP_PR_PULL_QUANT_STAR,
     Z3_OP_PR_PUSH_QUANT,
     Z3_OP_PR_ELIM_UNUSED_VARS,
     Z3_OP_PR_DER,
@@ -1159,8 +1142,6 @@ typedef enum {
     Z3_OP_PR_IFF_OEQ,
     Z3_OP_PR_NNF_POS,
     Z3_OP_PR_NNF_NEG,
-    Z3_OP_PR_NNF_STAR,
-    Z3_OP_PR_CNF_STAR,
     Z3_OP_PR_SKOLEMIZE,
     Z3_OP_PR_MODUS_PONENS_OEQ,
     Z3_OP_PR_TH_LEMMA,
@@ -1477,7 +1458,6 @@ extern "C" {
     /*@{*/
 
     /**
-        \deprecated
         \brief Create a configuration object for the Z3 context object.
 
         Configurations are created in order to assign parameters prior to creating
@@ -1510,7 +1490,6 @@ extern "C" {
     Z3_config Z3_API Z3_mk_config(void);
 
     /**
-        \deprecated
         \brief Delete the given configuration object.
 
         \sa Z3_mk_config
@@ -1520,7 +1499,6 @@ extern "C" {
     void Z3_API Z3_del_config(Z3_config c);
 
     /**
-        \deprecated
         \brief Set a configuration parameter.
 
         The following parameters can be set for
@@ -1537,7 +1515,6 @@ extern "C" {
     /*@{*/
 
     /**
-       \deprecated
        \brief Create a context using the given configuration.
 
        After a context is created, the configuration cannot be changed,
@@ -1617,7 +1594,6 @@ extern "C" {
     void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
 
     /**
-       \deprecated
        \brief Set a value of a context parameter.
 
        \sa Z3_global_param_set

src/api/z3_fpa.h

@@ -756,7 +756,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into an unsigned bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -772,7 +772,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a signed bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in signed 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -788,7 +788,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a real-numbered term.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         real number. Note that this type of conversion will often result in non-linear
         constraints over real terms.
 
@@ -1011,7 +1011,7 @@ extern "C" {
         determined.
 
         Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        knows only one NaN and it will always produce the same bit-vector represenatation of
+        knows only one NaN and it will always produce the same bit-vector representation of
         that NaN.
 
         def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))

src/api/z3_interp.h

@@ -98,7 +98,7 @@ extern "C" {
 
         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
+        must be generated by an SMT solver for which interpolation is
         supported, and the premises must be expressed using only
         theories and operators for which interpolation is supported.
 
@@ -199,7 +199,7 @@ extern "C" {
        (implies (and c1 ... cn f) v)
 
        where c1 .. cn are the children of v (which must precede v in the file)
-       and f is the formula assiciated to node v. The last formula in the
+       and f is the formula associated to node v. The last formula in the
        file is the root vertex, and is represented by the predicate "false".
 
        A solution to a tree interpolation problem can be thought of as a

src/ast/ast.cpp

@@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin():
     m_not_or_elim_decl(nullptr),
     m_rewrite_decl(nullptr),
     m_pull_quant_decl(nullptr),
-    m_pull_quant_star_decl(nullptr),
     m_push_quant_decl(nullptr),
     m_elim_unused_vars_decl(nullptr),
     m_der_decl(nullptr),
@@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_REWRITE:                      return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
     case PR_REWRITE_STAR:                 return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
     case PR_PULL_QUANT:                   return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
-    case PR_PULL_QUANT_STAR:              return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
     case PR_PUSH_QUANT:                   return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
     case PR_ELIM_UNUSED_VARS:             return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
     case PR_DER:                          return mk_proof_decl("der", k, 0, m_der_decl);
@@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_IFF_OEQ:                      return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
     case PR_NNF_POS:                      return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
     case PR_NNF_NEG:                      return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
-    case PR_NNF_STAR:                     return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
-    case PR_CNF_STAR:                     return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
     case PR_SKOLEMIZE:                    return mk_proof_decl("sk", k, 0, m_skolemize_decl);
     case PR_MODUS_PONENS_OEQ:             return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
     case PR_TH_LEMMA:                     return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
@@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
     DEC_REF(m_not_or_elim_decl);
     DEC_REF(m_rewrite_decl);
     DEC_REF(m_pull_quant_decl);
-    DEC_REF(m_pull_quant_star_decl);
     DEC_REF(m_push_quant_decl);
     DEC_REF(m_elim_unused_vars_decl);
     DEC_REF(m_der_decl);
@@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
     DEC_ARRAY_REF(m_apply_def_decls);
     DEC_ARRAY_REF(m_nnf_pos_decls);
     DEC_ARRAY_REF(m_nnf_neg_decls);
-    DEC_ARRAY_REF(m_nnf_star_decls);
-    DEC_ARRAY_REF(m_cnf_star_decls);
 
     DEC_ARRAY_REF(m_th_lemma_decls);
     DEC_REF(m_hyper_res_decl0);
@@ -1536,34 +1529,35 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
     // assigned in the order that they are created, this can result in differing
     // family ids. To avoid this, we first assign all family ids and only then inherit plugins.
     for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
-      symbol fid_name   = from.get_family_name(fid);
+        symbol fid_name   = from.get_family_name(fid);
-      if (!m_family_manager.has_family(fid)) {
+        if (!m_family_manager.has_family(fid)) {
-          family_id new_fid = mk_family_id(fid_name);
+            family_id new_fid = mk_family_id(fid_name);
-          (void)new_fid;
+            (void)new_fid;
-          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
+            TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
-      }
+        }
     }
     for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
-      SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
+        SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
-      SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
+        SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
-      symbol fid_name   = from.get_family_name(fid);
+        symbol fid_name   = from.get_family_name(fid);
-      TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
+        (void)fid_name;
-            << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
+        TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
-            if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
+              << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
-      TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
+              if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
-      SASSERT(fid == get_family_id(fid_name));
+        TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
-      if (from.has_plugin(fid) && !has_plugin(fid)) {
+        SASSERT(fid == get_family_id(fid_name));
-          decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
+        if (from.has_plugin(fid) && !has_plugin(fid)) {
-          register_plugin(fid, new_p);
+            decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
-          SASSERT(new_p->get_family_id() == fid);
+            register_plugin(fid, new_p);
-          SASSERT(has_plugin(fid));
+            SASSERT(new_p->get_family_id() == fid);
-      }
+            SASSERT(has_plugin(fid));
-      if (from.has_plugin(fid)) {
+        }
-          get_plugin(fid)->inherit(from.get_plugin(fid), trans);
+        if (from.has_plugin(fid)) {
-      }
+            get_plugin(fid)->inherit(from.get_plugin(fid), trans);
-      SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
+        }
-      SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
+        SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
-      SASSERT(!from.has_plugin(fid) || has_plugin(fid));
+        SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
+        SASSERT(!from.has_plugin(fid) || has_plugin(fid));
     }
 }
 
@@ -2843,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
     return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
 }
 
-proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
-    if (proofs_disabled())
-        return nullptr;
-    return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
-}
-
 proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
     if (proofs_disabled())
         return nullptr;
@@ -3093,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
     return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
 }
 
-proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (proofs_disabled())
-        return nullptr;
-    ptr_buffer<expr> args;
-    args.append(num_proofs, (expr**) proofs);
-    args.push_back(mk_oeq(s, t));
-    return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
-}
-
 proof * ast_manager::mk_skolemization(expr * q, expr * e) {
     if (proofs_disabled())
         return nullptr;
@@ -3110,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
     return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
 }
 
-proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (proofs_disabled())
-        return nullptr;
-    ptr_buffer<expr> args;
-    args.append(num_proofs, (expr**) proofs);
-    args.push_back(mk_oeq(s, t));
-    return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
-}
-
 proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
     if (proofs_disabled())
         return nullptr;

src/ast/ast.h

@@ -1042,11 +1042,11 @@ enum basic_op_kind {
 
     PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
     PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
-    PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
+    PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
 
     PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
 
-    PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
+    PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE, 
     PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
 };
 
@@ -1080,7 +1080,6 @@ protected:
     func_decl * m_not_or_elim_decl;
     func_decl * m_rewrite_decl;
     func_decl * m_pull_quant_decl;
-    func_decl * m_pull_quant_star_decl;
     func_decl * m_push_quant_decl;
     func_decl * m_elim_unused_vars_decl;
     func_decl * m_der_decl;
@@ -1106,8 +1105,6 @@ protected:
     ptr_vector<func_decl> m_apply_def_decls;
     ptr_vector<func_decl> m_nnf_pos_decls;
     ptr_vector<func_decl> m_nnf_neg_decls;
-    ptr_vector<func_decl> m_nnf_star_decls;
-    ptr_vector<func_decl> m_cnf_star_decls;
 
     ptr_vector<func_decl> m_th_lemma_decls;
     func_decl * m_hyper_res_decl0;
@@ -2182,7 +2179,6 @@ public:
     proof * mk_oeq_rewrite(expr * s, expr * t);
     proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_pull_quant(expr * e, quantifier * q);
-    proof * mk_pull_quant_star(expr * e, quantifier * q);
     proof * mk_push_quant(quantifier * q, expr * e);
     proof * mk_elim_unused_vars(quantifier * q, expr * r);
     proof * mk_der(quantifier * q, expr * r);
@@ -2201,9 +2197,8 @@ public:
 
     proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
-    proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_skolemization(expr * q, expr * e);
-    proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
+
 
     proof * mk_and_elim(proof * p, unsigned i);
     proof * mk_not_or_elim(proof * p, unsigned i);

src/ast/ast_pp_util.cpp

@@ -46,13 +46,18 @@ void ast_pp_util::display_decls(std::ostream& out) {
     n = coll.get_num_decls();
     for (unsigned i = 0; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
-        if (f->get_family_id() == null_family_id) {
+        if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
             ast_smt2_pp(out, f, env);
             out << "\n";
         }
     }
 }
 
+void ast_pp_util::remove_decl(func_decl* f) {
+    m_removed.insert(f);
+}
+
+
 void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
     if (neat) {
         smt2_pp_environment_dbg env(m);

src/ast/ast_pp_util.h

@@ -20,9 +20,11 @@ Revision History:
 #define AST_PP_UTIL_H_
 
 #include "ast/decl_collector.h"
+#include "util/obj_hashtable.h"
 
 class ast_pp_util {
     ast_manager&        m;
+    obj_hashtable<func_decl> m_removed;
  public:        
 
     decl_collector      coll;
@@ -35,6 +37,8 @@ class ast_pp_util {
 
     void collect(expr_ref_vector const& es);
 
+    void remove_decl(func_decl* f);
+
     void display_decls(std::ostream& out);
 
     void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);

src/ast/proofs/proof_checker.cpp

@@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m);); 
         return false;
     }
-    case PR_PULL_QUANT_STAR: {
-        if (match_proof(p) &&
-            match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2)) {
-            // TBD: check the enchilada.
-            return true;
-        }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m);); 
-        return false;
-    }
     case PR_PUSH_QUANT: {
         if (match_proof(p) &&
             match_fact(p, fact) &&
@@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // TBD:
         return true;
     }
-    case PR_NNF_STAR: {
-        // TBD:
-        return true;
-    }
     case PR_SKOLEMIZE: {
         // (exists ?x (p ?x y)) -> (p (sk y) y)
         // (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
@@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         UNREACHABLE();
         return false;
     }
-    case PR_CNF_STAR: {
-        for (unsigned i = 0; i < proofs.size(); ++i) {
-            if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
-                // ok
-            }
-            else {
-                UNREACHABLE();
-                return false;
-            }
-        }
-        // coarse grain CNF conversion.
-        return true;
-    }
     case PR_MODUS_PONENS_OEQ: {
         if (match_fact(p, fact) &&
             match_proof(p, p0, p1) &&
@@ -922,7 +895,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
     }
 }
 
-bool proof_checker::match_fact(proof* p, expr_ref& fact) {
+bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
     if (m.is_proof(p) &&
         m.has_fact(p)) {
         fact = m.get_fact(p);
@@ -938,13 +911,13 @@ void proof_checker::add_premise(proof* p) {
     }
 }
 
-bool proof_checker::match_proof(proof* p) {
+bool proof_checker::match_proof(proof const* p) const {
     return 
         m.is_proof(p) &&
         m.get_num_parents(p) == 0;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref& p0) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 1) {
         p0 = m.get_parent(p, 0);
@@ -953,7 +926,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
     return false;
 }
  
-bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 2) {
         p0 = m.get_parent(p, 0);
@@ -963,7 +936,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
     return false;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
+bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
     if (m.is_proof(p)) {
         for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
             parents.push_back(m.get_parent(p, i));
@@ -974,7 +947,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
 }
 
 
-bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_num_args() == 2) {
         d = to_app(e)->get_decl();
@@ -986,7 +959,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
 }
 
 
-bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) {
+bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP) {
         d = to_app(e)->get_decl();
         for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@@ -997,9 +970,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
     return false;
 }
 
-bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) {
+bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
     if (is_quantifier(e)) {
-        quantifier* q = to_quantifier(e);
+        quantifier const* q = to_quantifier(e);
         is_univ = q->is_forall();
         body = q->get_expr();
         for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@@ -1010,7 +983,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1022,7 +995,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
@@ -1035,7 +1008,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
 }
 
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1046,39 +1019,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
     return false;
 }
 
-bool proof_checker::match_not(expr* e, expr_ref& t) {
+bool proof_checker::match_not(expr const* e, expr_ref& t) const {
     return match_op(e, OP_NOT, t);
 }
 
-bool proof_checker::match_or(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_OR, terms);
 }
 
-bool proof_checker::match_and(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_AND, terms);
 }
 
-bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IFF, t1, t2);
 }
 
-bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
 }
 
-bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IMPLIES, t1, t2);
 }
 
-bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
 }
 
-bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_OEQ, t1, t2);
 }
 
-bool proof_checker::match_negated(expr* a, expr* b) {
+bool proof_checker::match_negated(expr const* a, expr* b) const {
     expr_ref t(m);
     return 
         (match_not(a, t) && t.get() == b) ||
@@ -1186,14 +1159,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
 
 }
 
-bool proof_checker::match_nil(expr* e) const {
+bool proof_checker::match_nil(expr const* e) const {
     return 
         is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_NIL;
 }
 
-bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
+bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_CONS) {
@@ -1205,7 +1178,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
 }
 
 
-bool proof_checker::match_atom(expr* e, expr_ref& a) const {
+bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_ATOM) {
@@ -1227,7 +1200,7 @@ expr* proof_checker::mk_nil() {
     return m_nil.get();
 }
 
-bool proof_checker::is_hypothesis(proof* p) const {
+bool proof_checker::is_hypothesis(proof const* p) const {
     return 
         m.is_proof(p) &&
         p->get_decl_kind() == PR_HYPOTHESIS;
@@ -1253,7 +1226,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
     } 
 }
 
-void proof_checker::dump_proof(proof * pr) {
+void proof_checker::dump_proof(proof const* pr) {
     if (!m_dump_lemmas)
         return;
     SASSERT(m.has_fact(pr));

src/ast/proofs/proof_checker.h

@@ -77,39 +77,39 @@ private:
     bool check1_spc(proof* p, expr_ref_vector& side_conditions);
     bool check_arith_proof(proof* p);
     bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
-    bool match_fact(proof* p, expr_ref& fact);
+    bool match_fact(proof const* p, expr_ref& fact) const;
     void add_premise(proof* p);
-    bool match_proof(proof* p);
+    bool match_proof(proof const* p) const;
-    bool match_proof(proof* p, proof_ref& p0);
+    bool match_proof(proof const* p, proof_ref& p0) const;
-    bool match_proof(proof* p, proof_ref& p0, proof_ref& p1);
+    bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
-    bool match_proof(proof* p, proof_ref_vector& parents);
+    bool match_proof(proof const* p, proof_ref_vector& parents) const;
-    bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2);
+    bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2);
+    bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr* e, decl_kind k, expr_ref& t);
+    bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
-    bool match_op(expr* e, decl_kind k, expr_ref_vector& terms);
+    bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
-    bool match_iff(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_implies(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_eq(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_not(expr* e, expr_ref& t);
+    bool match_not(expr const* e, expr_ref& t) const;
-    bool match_or(expr* e, expr_ref_vector& terms);
+    bool match_or(expr const* e, expr_ref_vector& terms) const;
-    bool match_and(expr* e, expr_ref_vector& terms);
+    bool match_and(expr const* e, expr_ref_vector& terms) const;
-    bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms);
+    bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
-    bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body);
+    bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
-    bool match_negated(expr* a, expr* b);
+    bool match_negated(expr const* a, expr* b) const;
-    bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2);
+    bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
     void get_ors(expr* e, expr_ref_vector& ors);
     void get_hypotheses(proof* p, expr_ref_vector& ante);
 
-    bool match_nil(expr* e) const;
+    bool match_nil(expr const* e) const;
-    bool match_cons(expr* e, expr_ref& a, expr_ref& b) const;
+    bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
-    bool match_atom(expr* e, expr_ref& a) const;
+    bool match_atom(expr const* e, expr_ref& a) const;
     expr* mk_nil();
     expr* mk_cons(expr* a, expr* b);
     expr* mk_atom(expr* e);
-    bool is_hypothesis(proof* p) const;
+    bool is_hypothesis(proof const* p) const;
     expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
-    void dump_proof(proof * pr);
+    void dump_proof(proof const* pr);
     void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
 
     void set_false(expr_ref& e, unsigned idx, expr_ref& lit);

src/ast/rewriter/rewriter_def.h

@@ -358,7 +358,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 if (ProofGen) {
                     NOT_IMPLEMENTED_YET();
                     // We do not support the use of bindings in proof generation mode.
-                    // Thus we have to apply the subsitution here, and
+                    // Thus we have to apply the substitution here, and
                     // beta_reducer subst(m());
                     // subst.set_bindings(new_num_args, new_args);
                     // expr_ref r2(m());

src/interp/iz3checker.cpp

@@ -43,7 +43,7 @@ struct iz3checker : iz3base {
     /* HACK: for tree interpolants, we assume that uninterpreted functions
        are global. This is because in the current state of the tree interpolation
        code, symbols that appear in sibling sub-trees have to be global, and
-       we have no way to eliminate such function symbols. When tree interpoaltion is
+       we have no way to eliminate such function symbols. When tree interpolation is
        fixed, we can tree function symbols the same as constant symbols. */
 
     bool is_tree;

src/math/polynomial/upolynomial.cpp

@@ -781,17 +781,15 @@ namespace upolynomial {
                 set(q.size(), q.c_ptr(), C);
                 m().set(bound, p);
             }
+            else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) {
+                // discard accumulated image, it was affected by unlucky primes
+                TRACE("mgcd", tout << "discarding image\n";);
+                set(q.size(), q.c_ptr(), C);
+                m().set(bound, p);
+            }
             else {
-                if (q.size() < C.size()) {
+                CRA_combine_images(q, p, C, bound);
-                    // discard accumulated image, it was affected by unlucky primes
+                TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
-                    TRACE("mgcd", tout << "discarding image\n";);
-                    set(q.size(), q.c_ptr(), C);
-                    m().set(bound, p);
-                }
-                else {
-                    CRA_combine_images(q, p, C, bound);
-                    TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
-                }
             }
             numeral_vector & candidate = q;
             get_primitive(C, candidate);

src/muz/base/dl_context.cpp

@@ -1106,6 +1106,16 @@ namespace datalog {
             names.push_back(m_rule_names[i]);            
         }
     }
+
+    static std::ostream& display_symbol(std::ostream& out, symbol const& nm) {
+        if (is_smt2_quoted_symbol(nm)) {
+            out << mk_smt2_quoted_symbol(nm);
+        }
+        else {
+            out << nm;
+        }
+        return out;
+    }
  
     void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
         ast_manager& m = get_manager();
@@ -1148,13 +1158,13 @@ namespace datalog {
         if (!use_fixedpoint_extensions) {
             out << "(set-logic HORN)\n";
         }
+        for (func_decl * f : rels) 
+            visitor.remove_decl(f);
 
         visitor.display_decls(out);
-        func_decl_set::iterator it = rels.begin(), end = rels.end();
+
-        for (; it != end; ++it) {
+        for (func_decl * f : rels) 
-            func_decl* f = *it;
             display_rel_decl(out, f);
-        }
 
         if (use_fixedpoint_extensions && do_declare_vars) {
             declare_vars(rules, fresh_names, out);
@@ -1185,13 +1195,7 @@ namespace datalog {
                     nm = symbol(s.str().c_str());                    
                 }
                 fresh_names.add(nm);
-                if (is_smt2_quoted_symbol(nm)) {
+                display_symbol(out, nm) << ")";
-                    out << mk_smt2_quoted_symbol(nm);
-                }
-                else {
-                    out << nm;
-                }
-                out << ")";
             }
             out << ")\n";
         }
@@ -1219,7 +1223,8 @@ namespace datalog {
                     PP(qfn);
                     out << ")\n";
                 }
-                out << "(query " << fn->get_name() << ")\n";
+                out << "(query ";
+                display_symbol(out, fn->get_name()) << ")\n";
             }
         }
         else {
@@ -1238,7 +1243,8 @@ namespace datalog {
 
     void context::display_rel_decl(std::ostream& out, func_decl* f) {
         smt2_pp_environment_dbg env(m);
-        out << "(declare-rel " << f->get_name() << " (";
+        out << "(declare-rel ";
+        display_symbol(out, f->get_name()) << " (";
         for (unsigned i = 0; i < f->get_arity(); ++i) {                
             ast_smt2_pp(out, f->get_domain(i), env);
             if (i + 1 < f->get_arity()) {

src/muz/base/fixedpoint_params.pyg

@@ -33,7 +33,7 @@ def_module_params('fixedpoint',
                            "updated relation was modified or not"),
                           ('datalog.compile_with_widening', BOOL, False, 
                            "widening will be used to compile recursive rules"),
-                          ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
+                          ('datalog.default_table_checked', BOOL, False, "if true, the default " +
                            'table will be default_table inside a wrapper that checks that its results ' +
                            'are the same as of default_table_checker table'),
                           ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
@@ -59,7 +59,7 @@ def_module_params('fixedpoint',
                           ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
                           ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
                           ('duality.feasible_edges', BOOL, True, 
-                           'Don\'t expand definitley infeasible edges'),
+                           'Don\'t expand definitely infeasible edges'),
                           ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
                           ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
                           ('duality.recursion_bound', UINT, UINT_MAX, 
@@ -130,7 +130,7 @@ def_module_params('fixedpoint',
                           ('xform.magic', BOOL, False, 
                            "perform symbolic magic set transformation"),
                           ('xform.scale', BOOL, False, 
-                           "add scaling variable to linear real arithemtic clauses"),
+                           "add scaling variable to linear real arithmetic clauses"),
                           ('xform.inline_linear', BOOL, True, "try linear inlining method"),
                           ('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
                           ('xform.inline_linear_branch', BOOL, False, 
@@ -176,7 +176,7 @@ def_module_params('fixedpoint',
                           ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
                           ('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
                           ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
-                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"),
+                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
                           ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
                           ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
                           ('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"),

src/muz/transforms/dl_mk_array_instantiation.h

@@ -26,7 +26,7 @@ Implementation:
 
     1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
 
-    2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
+    2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
        P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
        corresponds to fixedpoint.xform.instantiate_arrays.enforce
 

src/muz/transforms/dl_mk_interp_tail_simplifier.h

@@ -53,7 +53,7 @@ namespace datalog {
             */
             void reset(rule * r);
 
-            /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+            /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
             bool unify(expr * e1, expr * e2);
 
             void get_result(rule_ref & res);

src/muz/transforms/dl_mk_rule_inliner.h

@@ -45,7 +45,7 @@ namespace datalog {
             : m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx), 
             m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
             
-        /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+        /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
         bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
 
         /**

src/muz/transforms/dl_mk_scale.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Add scale factor to linear (Real) arithemetic Horn clauses.
+    Add scale factor to linear (Real) arithmetic Horn clauses.
     The transformation replaces occurrences of isolated constants by
     a scale multiplied to each constant. 
 

src/smt/theory_arith_core.h

@@ -469,7 +469,8 @@ namespace smt {
         if (negated) l_conseq.neg();
 
         TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
-              tout << s_ante << "\n" << s_conseq << "\n";);
+              tout << s_ante << "\n" << s_conseq << "\n";
+              tout << l_ante << "\n" << l_conseq << "\n";);
 
         // literal lits[2] = {l_ante, l_conseq};
         mk_clause(l_ante, l_conseq, 0, nullptr);
@@ -589,13 +590,13 @@ namespace smt {
     }
 
     //
-    // create the term: s := to_real(to_int(x)) - x
+    // create the term: s := x - to_real(to_int(x))
     // add the bounds 0 <= s < 1   
     //
     template<typename Ext>
     void theory_arith<Ext>::mk_to_int_axiom(app * n) {
         SASSERT(m_util.is_to_int(n));
-        ast_manager & m    = get_manager();
+        ast_manager & m  = get_manager();
         expr* x = n->get_arg(0);
 
         // to_int (to_real x) = x
@@ -603,11 +604,15 @@ namespace smt {
             mk_axiom(m.mk_false(), m.mk_eq(to_app(x)->get_arg(0), n));
             return;
         }
-        expr* to_r = m_util.mk_to_real(n);
+        expr_ref to_r(m_util.mk_to_real(n), m);
-        expr_ref lo(m_util.mk_le(to_r, x), m);
+        expr_ref diff(m_util.mk_add(x, m_util.mk_mul(m_util.mk_real(-1), to_r)), m);
-        expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
+        
-        mk_axiom(m.mk_false(), lo);
+        expr_ref lo(m_util.mk_ge(diff, m_util.mk_real(0)), m);
-        mk_axiom(m.mk_false(), hi);
+        expr_ref hi(m_util.mk_ge(diff, m_util.mk_real(1)), m);
+        hi = m.mk_not(hi);
+
+        mk_axiom(m.mk_false(), lo, false);
+        mk_axiom(m.mk_false(), hi, false);
     }
 
     template<typename Ext>
@@ -1202,7 +1207,7 @@ namespace smt {
 
     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";);
+        TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
         context & ctx = get_context();
         SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n));
         SASSERT(!ctx.b_internalized(n));

src/smt/theory_str.cpp

@@ -641,7 +641,6 @@ namespace smt {
     }
 
     app * theory_str::mk_indexof(expr * haystack, expr * needle) {
-        // TODO check meaning of the third argument here
         app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
         m_trail.push_back(indexof);
         // immediately force internalization so that axiom setup does not fail
@@ -844,14 +843,7 @@ namespace smt {
                     instantiate_axiom_Contains(e);
                 } else if (u.str.is_index(a)) {
                     instantiate_axiom_Indexof(e);
-                    /* TODO NEXT: Indexof2/Lastindexof rewrite?
-                       } else if (is_Indexof2(e)) {
-                       instantiate_axiom_Indexof2(e);
-                       } else if (is_LastIndexof(e)) {
-                       instantiate_axiom_LastIndexof(e);
-                    */
                 } else if (u.str.is_extract(a)) {
-                    // TODO check semantics of substr vs. extract
                     instantiate_axiom_Substr(e);
                 } else if (u.str.is_replace(a)) {
                     instantiate_axiom_Replace(e);
@@ -1232,27 +1224,37 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        app * expr = e->get_owner();
+        app * ex = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
+        if (axiomatized_terms.contains(ex)) {
-            TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+            TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
             return;
         }
-        axiomatized_terms.insert(expr);
+        SASSERT(ex->get_num_args() == 3);
+        // if the third argument is exactly the integer 0, we can use this "simple" indexof;
+        // otherwise, we call the "extended" version
+        expr * startingPosition = ex->get_arg(2);
+        rational startingInteger;
+        if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) {
+            // "extended" indexof term with prefix
+            instantiate_axiom_Indexof_extended(e);
+            return;
+        }
+        axiomatized_terms.insert(ex);
 
-        TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
 
         expr_ref x1(mk_str_var("x1"), m);
         expr_ref x2(mk_str_var("x2"), m);
         expr_ref indexAst(mk_int_var("index"), m);
 
-        expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
+        expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
         SASSERT(condAst);
 
         // -----------------------
         // true branch
         expr_ref_vector thenItems(m);
         //  args[0] = x1 . args[1] . x2
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
         //  indexAst = |x1|
         thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
         //     args[0]  = x3 . x4
@@ -1260,11 +1262,11 @@ namespace smt {
         //  /\ ! contains(x3, args[1])
         expr_ref x3(mk_str_var("x3"), m);
         expr_ref x4(mk_str_var("x4"), m);
-        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
+        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
         SASSERT(tmpLen);
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
         expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
         SASSERT(thenBranch);
 
@@ -1276,26 +1278,42 @@ namespace smt {
         expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m);
         SASSERT(breakdownAssert);
 
-        expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m);
+        expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m);
         SASSERT(reduceToIndex);
 
         expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
         SASSERT(finalAxiom);
         assert_axiom(finalAxiom);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m);
+            expr_ref zeroAst(mk_int(0), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
-    void theory_str::instantiate_axiom_Indexof2(enode * e) {
+    void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
         app * expr = e->get_owner();
         if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+            TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
             return;
         }
+        SASSERT(expr->get_num_args() == 3);
         axiomatized_terms.insert(expr);
 
-        TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
 
         // -------------------------------------------------------------------------------
         //   if (arg[2] >= length(arg[0]))                          // ite2
@@ -1327,7 +1345,7 @@ namespace smt {
         ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
         ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
         ite2ElseItems.push_back(ite3);
-        expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
+        expr_ref ite2Else(mk_and(ite2ElseItems), m);
         SASSERT(ite2Else);
 
         expr_ref ite2(m.mk_ite(
@@ -1350,6 +1368,20 @@ namespace smt {
         expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
         SASSERT(reduceTerm);
         assert_axiom(reduceTerm);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
     void theory_str::instantiate_axiom_LastIndexof(enode * e) {
@@ -5521,7 +5553,8 @@ namespace smt {
         return node;
     }
 
-    void theory_str::get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
+    void theory_str::get_grounded_concats(unsigned depth,
+                                          expr* node, std::map<expr*, expr*> & varAliasMap,
                                           std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
                                           std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
                                           std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) {
@@ -5536,6 +5569,9 @@ namespace smt {
         if (groundedMap.find(node) != groundedMap.end()) {
             return;
         }
+        IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n";
+                   if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n";
+                   );
 
         // haven't computed grounded concats for "node" (de-aliased)
         // ---------------------------------------------------------
@@ -5565,8 +5601,8 @@ namespace smt {
                 expr * arg1 = to_app(node)->get_arg(1);
                 expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
                 expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
-                get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
-                get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin();
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator arg1_grdItor;
@@ -5616,7 +5652,7 @@ namespace smt {
             else if (varEqConcatMap.find(node) != varEqConcatMap.end()) {
                 expr * eqConcat = varEqConcatMap[node].begin()->first;
                 expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap);
-                get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator grdItor = groundedMap[deAliasedEqConcat].begin();
                 for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) {
@@ -5825,8 +5861,8 @@ namespace smt {
             expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
             expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
 
-            get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+            get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
-            get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+            get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
             // debugging
             print_grounded_concat(strDeAlias, groundedMap);
@@ -8731,8 +8767,8 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        expr_ref_vector assignments(m);
+        //expr_ref_vector assignments(m);
-        ctx.get_assignments(assignments);
+        //ctx.get_assignments(assignments);
 
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = false;

src/smt/theory_str.h

@@ -447,7 +447,7 @@ protected:
     void instantiate_axiom_suffixof(enode * e);
     void instantiate_axiom_Contains(enode * e);
     void instantiate_axiom_Indexof(enode * e);
-    void instantiate_axiom_Indexof2(enode * e);
+    void instantiate_axiom_Indexof_extended(enode * e);
     void instantiate_axiom_LastIndexof(enode * e);
     void instantiate_axiom_Substr(enode * e);
     void instantiate_axiom_Replace(enode * e);
@@ -495,10 +495,11 @@ protected:
             std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
             std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
     expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
-    void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
+    void get_grounded_concats(unsigned depth,
-            std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
+                              expr* node, std::map<expr*, expr*> & varAliasMap,
-            std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
+                              std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
-            std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+                              std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
+                              std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
     void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
     void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
             std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);

src/tactic/aig/aig.cpp

@@ -267,7 +267,7 @@ struct aig_manager::imp {
             }
             if  (b == r) {
                 if (sign1) {
-                    // subsitution
+                    // substitution
                     // not (a and b) and r --> (not a) and r   IF b == r
                     l = a;
                     l.invert();

src/tactic/core/ctx_simplify_tactic.cpp

@@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp {
             for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
                 expr * t = g.form(i);
                 process(t, r);
-                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-)
+                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
                 g.update(i, r, new_pr, g.dep(i));
             }
         }

src/tactic/core/dom_simplify_tactic.cpp

@@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             change |= r != g.form(i);
             proof* new_pr = nullptr;
             if (g.proofs_enabled()) {
-                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
             }
             g.update(i, r, new_pr, g.dep(i));
         }
@@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
             proof* new_pr = nullptr;
             if (g.proofs_enabled()) {
-                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
             }
             g.update(i, r, new_pr, g.dep(i));
         }

src/tactic/tactic_exception.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Tactic expection object.
+    Tactic exception object.
 
 Author:
 

src/tactic/tactical.h

@@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
 
 tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
 /**
-   \brief Fails if \c t produeces more than \c threshold subgoals.
+   \brief Fails if \c t produces more than \c threshold subgoals.
    Otherwise, it behaves like \c t.
 */
 tactic * fail_if_branching(tactic * t, unsigned threshold = 1);

src/test/quant_elim.cpp

@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 
 
+#if 0
 static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
 
     //    enable_trace("bit2int");
@@ -48,6 +49,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
         //exit(-1);
     }
 }
+#endif
 
 static void test_formula(lbool expected_outcome, char const* fml) {
     ast_manager m;

src/util/scoped_timer.cpp

@@ -33,8 +33,8 @@ Revision History:
 #include<sys/time.h>
 #include<sys/errno.h>
 #include<pthread.h>
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_)
-// Linux
+// Linux & FreeBSD & NetBSD
 #include<errno.h>
 #include<pthread.h>
 #include<sched.h>
@@ -66,8 +66,8 @@ struct scoped_timer::imp {
     pthread_mutex_t  m_mutex;
     pthread_cond_t   m_condition_var;
     struct timespec  m_end_time;
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-    // Linux & FreeBSD
+    // Linux & FreeBSD & NetBSD
     pthread_t       m_thread_id;
     pthread_mutex_t m_mutex;
     pthread_cond_t  m_cond;
@@ -104,7 +104,7 @@ struct scoped_timer::imp {
 
         return st;
     }
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
     static void* thread_func(void *arg) {
         scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
 
@@ -175,8 +175,8 @@ struct scoped_timer::imp {
 
         if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
             throw default_exception("failed to start timer thread");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-        // Linux & FreeBSD
+        // Linux & FreeBSD & NetBSD
         m_ms = ms;
         m_initialized = false;
         m_signal_sent = false;
@@ -216,8 +216,8 @@ struct scoped_timer::imp {
             throw default_exception("failed to destroy pthread condition variable");
         if (pthread_attr_destroy(&m_attributes) != 0)
             throw default_exception("failed to destroy pthread attributes object");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
-        // Linux & FreeBSD
+        // Linux & FreeBSD & NetBSD
         bool init = false;
 
         // spin until timer thread has been created

src/util/stopwatch.h

@@ -134,6 +134,11 @@ public:
 
 #include<ctime>
 
+#ifndef CLOCK_PROCESS_CPUTIME_ID
+/* BSD */
+# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
+#endif
+
 class stopwatch {
     unsigned long long m_time; // elapsed time in ns
     bool               m_running;