Merge remote-tracking branch 'upstream/master' into lackr

README

@@ -1,53 +0,0 @@
-Z3 is a theorem prover from Microsoft Research.
-Z3 is licensed under the MIT license. 
-Z3 can be built using Visual Studio Command Prompt and make/g++.
-
-1) Building Z3 on Windows using Visual Studio Command Prompt
-   
-32-bit builds, start with:
-
-   python scripts/mk_make.py
-
-or instead, for a 64-bit build:
-
-   python scripts/mk_make.py -x
-
-then:
-
-   cd build
-   nmake
-
-2) Building Z3 using make/g++ and Python
-Execute:
-
-   python scripts/mk_make.py
-   cd build
-   make
-   sudo make install
-
-By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include,
-where PREFIX is the installation prefix used for installing Python in your system.
-It is usually /usr for most Linux distros, and /usr/local for FreeBSD.
-Use the following commands to install in a different prefix (e.g., /home/leo)
-
-  python scripts/mk_make.py --prefix=/home/leo
-  cd build
-  make
-  make install
-
-In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages,
-where X.Y corresponds to the python version in your system.
-
-To uninstall Z3, use
-
-  sudo make uninstall
-
-4) Building Z3 using clang and clang++ on Linux/OSX
-Remark: clang does not support OpenMP yet.   
-
-   CXX=clang++ CC=clang python scripts/mk_make.py
-   cd build
-   make
-
-
-To clean Z3 you can delete the build directory and run the mk_make.py script again.

README.md

@@ -0,0 +1,161 @@
+# Z3
+
+Z3 is a theorem prover from Microsoft Research. It is licensed
+under the [MIT license](LICENSE.txt).
+
+Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides
+[bindings for several programming languages][3].
+
+See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3.
+
+[1]: #building-z3-on-windows-using-visual-studio-command-prompt
+[2]: #building-z3-using-make-and-gccclang
+[3]: #z3-bindings
+
+## Building Z3 on Windows using Visual Studio Command Prompt
+
+32-bit builds, start with:
+
+```bash
+python scripts/mk_make.py
+```
+
+or instead, for a 64-bit build:
+
+```bash
+python scripts/mk_make.py -x
+```
+
+then:
+
+```bash
+cd build
+nmake
+```
+
+## Building Z3 using make and GCC/Clang
+
+Execute:
+
+```bash
+python scripts/mk_make.py
+cd build
+make
+sudo make install
+```
+
+Note by default ``gcc`` is used as the C++ compiler if it is available. If you
+would prefer to use Clang change the ``mk_make.py`` line to
+
+```bash
+CXX=clang++ CC=clang python scripts/mk_make.py
+```
+
+Note that Clang < 3.7 does not support OpenMP.
+
+By default, it will install z3 executable at ``PREFIX/bin``, libraries at
+``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX``
+installation prefix if inferred by the ``mk_make.py`` script. It is usually
+``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use
+the ``--prefix=`` command line option to change the install prefix. For example:
+
+```bash
+python scripts/mk_make.py --prefix=/home/leo
+cd build
+make
+make install
+```
+
+Note the above will typically disable the installation of the Python bindings
+because the Python ``site-packages``  directory (e.g.
+``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and
+installing outside of the install prefix is dangerous and misleading.
+
+To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the
+install prefix as the default. The ``DESTDIR`` variable is prepended to the
+install locations during ``make install`` and ``make uninstall`` and is intended
+to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html).
+Therefore it must always contain a trailing slash.
+
+For example:
+
+```bash
+python scripts/mk_make.py
+cd build
+make
+make install DESTDIR=/home/leo/
+```
+
+In this example, the Z3 Python bindings will be stored at
+``/home/leo/lib/pythonX.Y/site-packages``
+(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux
+distributions) where X.Y corresponds to the python version in your system.
+
+To uninstall Z3, use
+
+```bash
+sudo make uninstall
+```
+
+To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again.
+
+## Z3 bindings
+
+Z3 has bindings for various programming languages.
+
+### ``.NET``
+
+These bindings are enabled by default on Windows and are enabled on other
+platforms if [mono](http://www.mono-project.com/) is detected. On these
+platforms the location of the C# compiler and gac utility need to be known. You
+can set these as follows if they aren't detected automatically. For example:
+
+```bash
+CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py
+```
+
+To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``.
+
+Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC``
+to ``/usr/bin/dmcs``.
+
+Note that when ``make install`` is executed on non-windows platforms the GAC
+utility is used to install ``Microsoft.Z3.dll`` into the
+[GAC](http://www.mono-project.com/docs/advanced/assemblies-and-the-gac/) as the
+``Microsoft.Z3.Sharp`` package. During install a
+[pkg-config](http://www.freedesktop.org/wiki/Software/pkg-config/) file
+(``Microsoft.Z3.Sharp.pc``) is also installed which allows the
+[MonoDevelop](http://www.monodevelop.com/) IDE to find the bindings. Running
+``make uninstall`` will remove the dll from the GAC and the pkg-config file.
+
+See [``examples/dotnet``](examples/dotnet) for examples.
+
+### ``C``
+
+These are always enabled.
+
+See [``examples/c``](examples/c) for examples.
+
+### ``C++``
+
+These are always enabled.
+
+See [``examples/c++``](examples/c++) for examples.
+
+### ``Java``
+
+Use the ``--java`` command line flag with ``mk_make.py`` to enable building these.
+
+See [``examples/java``](examples/java) for examples.
+
+### ``OCaml``
+
+Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these.
+
+See [``examples/ml``](examples/ml) for examples.
+
+### ``Python``
+
+These bindings are always enabled.
+
+See [``examples/python``](examples/python) for examples.

scripts/mk_util.py

@@ -79,7 +79,7 @@ TRACE = False
 DOTNET_ENABLED=False
 JAVA_ENABLED=False
 ML_ENABLED=False
-PYTHON_INSTALL_ENABLED=True
+PYTHON_INSTALL_ENABLED=False
 STATIC_LIB=False
 VER_MAJOR=None
 VER_MINOR=None
@@ -612,6 +612,7 @@ def display_help(exit_code):
     print("  --dotnet                      generate .NET bindings.")
     print("  --java                        generate Java bindings.")
     print("  --ml                          generate OCaml bindings.")
+    print("  --python                      generate Python bindings.")
     print("  --staticlib                   build Z3 static library.")
     if not IS_WINDOWS:
         print("  -g, --gmp                     use GMP.")
@@ -642,14 +643,14 @@ def display_help(exit_code):
 # Parse configuration option for mk_make script
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
-    global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
+    global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
                                                 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
-                                                'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir='])
+                                                'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python'])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
@@ -708,6 +709,8 @@ def parse_options():
             ML_ENABLED = True
         elif opt in ('', '--noomp'):
             USE_OMP = False
+        elif opt in ('--python'):
+            PYTHON_INSTALL_ENABLED = True
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
@@ -1339,6 +1342,9 @@ class PythonInstallComponent(Component):
         self.in_prefix_install = True
         self.libz3Component = libz3Component
 
+        if not PYTHON_INSTALL_ENABLED:
+            return
+
         if IS_WINDOWS:
             # Installing under Windows doesn't make sense as the install prefix is used
             # but that doesn't make sense under Windows
@@ -1357,7 +1363,15 @@ class PythonInstallComponent(Component):
         else:
             # Use path inside the prefix (should be the normal case on Linux)
             # CMW: Also normal on *BSD?
-            assert PYTHON_PACKAGE_DIR.startswith(PREFIX)
+            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+                raise MKException(('The python package directory ({}) must live ' +
+                    'under the install prefix ({}) to install the python bindings.' +
+                    'Use --pypkgdir and --prefix to set the python package directory ' +
+                    'and install prefix respectively. Note that the python package ' +
+                    'directory does not need to exist and will be created if ' +
+                    'necessary during install.').format(
+                        PYTHON_PACKAGE_DIR,
+                        PREFIX))
             self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             self.in_prefix_install = True
 
@@ -1365,7 +1379,7 @@ class PythonInstallComponent(Component):
             assert not os.path.isabs(self.pythonPkgDir)
 
     def final_info(self):
-        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+        if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED:
             print("Warning: The detected Python package directory (%s) is not "
                   "in the installation prefix (%s). This can lead to a broken "
                   "Python API installation. Use --pypkgdir= to change the "

src/api/ml/z3.ml

@@ -789,6 +789,8 @@ sig
   val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr 
   val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) 
                   -> expr -> expr -> expr -> expr 
+  val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) 
+                  -> expr -> expr -> expr -> expr -> expr
   val compare : expr -> expr -> int
 end = struct  
   type expr = Expr of AST.ast
@@ -797,6 +799,12 @@ end = struct
   let gnc e = match e with Expr(a) -> (z3obj_gnc a)
   let gno e = match e with Expr(a) -> (z3obj_gno a)
 
+  let inc_elist (es : expr list) = 
+      List.iter (fun e -> match e with Expr(o) -> o.inc_ref (gnc e) o.m_n_obj) es
+
+  let dec_elist (es : expr list) = 
+      List.iter (fun e -> match e with Expr(o) -> o.dec_ref (gnc e) o.m_n_obj) es
+
   let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> 
     let e = z3_native_object_of_ast_ptr ctx no in 
     if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then
@@ -850,6 +858,9 @@ end = struct
   let apply3 ctx f t1 t2 t3 = 
       expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3))
 
+  let apply4 ctx f t1 t2 t3 t4 = 
+      expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3) (gno t4))
+
   let simplify ( x : expr ) ( p : Params.params option ) = match p with 
     | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x))
     | Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp))
@@ -871,19 +882,30 @@ end = struct
     if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then
       raise (Z3native.Exception "Number of arguments does not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) 
+      (inc_elist args; 
+       let r = expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) in
+       dec_elist args;
+       r)
       
   let substitute ( x : expr ) from to_ = 
     if (List.length from) <> (List.length to_) then
       raise (Z3native.Exception "Argument sizes do not match")
     else
-      expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) 
+      (inc_elist from;
+       inc_elist to_;
+       let r = expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) in
+       dec_elist from;
+       dec_elist to_;
+       r)
      
   let substitute_one ( x : expr ) from to_ =
     substitute ( x : expr ) [ from ] [ to_ ]
       
   let substitute_vars ( x : expr ) to_ =
-    expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_))
+    (inc_elist to_;
+     let r = expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_)) in
+     dec_elist to_;
+     r)
       
   let translate ( x : expr ) to_ctx =
     if (Expr.gc x) == to_ctx then
@@ -1258,21 +1280,20 @@ struct
   let mk_union  ( ctx : context ) ( args : expr list ) =
     expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) 
           
-      
   let mk_intersection  ( ctx : context ) ( args : expr list ) =
     expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args))
 
   let mk_difference  ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_difference (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
+    apply2 ctx Z3native.mk_set_difference arg1 arg2
 
   let mk_complement  ( ctx : context ) ( arg : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_complement (context_gno ctx) (Expr.gno arg))
+    apply1 ctx Z3native.mk_set_complement arg
 
   let mk_membership  ( ctx : context ) ( elem : expr ) ( set : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_member (context_gno ctx) (Expr.gno elem) (Expr.gno set))
+    apply2 ctx Z3native.mk_set_member elem set
 
   let mk_subset  ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_set_subset (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2))
+    apply2 ctx Z3native.mk_set_subset arg1 arg2
 
 end
 
@@ -1612,10 +1633,10 @@ struct
       mk_const ctx (Symbol.mk_string ctx name)
      
     let mk_mod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =    
-      expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+      apply2 ctx Z3native.mk_mod t1 t2
      
     let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-      expr_of_ptr  ctx (Z3native.mk_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+      apply2 ctx Z3native.mk_rem t1 t2
 
     let mk_numeral_s ( ctx : context ) ( v : string ) =
       expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx)))
@@ -1624,7 +1645,7 @@ struct
       expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx)))
 
     let mk_int2real ( ctx : context ) ( t : expr ) =
-      (Expr.expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (Expr.gno t)))
+      apply1 ctx Z3native.mk_int2real t
 
     let mk_int2bv ( ctx : context ) ( n : int ) ( t : expr ) =
       (Expr.expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (Expr.gno t)))
@@ -1636,10 +1657,10 @@ struct
       Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx))     
 
     let get_numerator ( x : expr ) =
-      expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x))
+      apply1 (Expr.gc x) Z3native.get_numerator x
      
     let get_denominator ( x : expr ) =
-      expr_of_ptr (Expr.gc x) (Z3native.get_denominator (Expr.gnc x) (Expr.gno x))
+      apply1 (Expr.gc x) Z3native.get_denominator x
      
     let get_ratio ( x : expr ) = 
       if (is_rat_numeral x)  then
@@ -1671,10 +1692,10 @@ struct
       expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx)))
      
     let mk_is_integer ( ctx : context ) ( t : expr ) =
-      (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (Expr.gno t)))
+      apply1 ctx Z3native.mk_is_int t
      
     let mk_real2int ( ctx : context ) ( t : expr ) =
-      (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t)))
+      apply1 ctx Z3native.mk_real2int t
 
     module AlgebraicNumber =
     struct    
@@ -1703,26 +1724,19 @@ struct
     let f x = (Expr.gno x) in
     (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (List.length t) (Array.of_list (List.map f t))))
       
-  let mk_unary_minus ( ctx : context ) ( t : expr ) =     
+  let mk_unary_minus ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_unary_minus t
-    (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (Expr.gno t)))
 
-  let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_div t1 t2
-    (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
 
-  let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =     
+  let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_power t1 t2
-    (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
 
-  let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_lt t1 t2
-    (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
 
-  let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_le t1 t2
-    (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
       
-  let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_gt t1 t2
-    (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
 
-  let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ge t1 t2
-    (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
 end
 
 
@@ -1793,60 +1807,33 @@ struct
     Expr.mk_const ctx name (mk_sort ctx size) 
   let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) =
     mk_const ctx (Symbol.mk_string ctx name) size
-  let mk_not  ( ctx : context ) ( t : expr ) =
+  let mk_not  ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvnot t
-    expr_of_ptr ctx (Z3native.mk_bvnot (context_gno ctx) (Expr.gno t))
+  let mk_redand  ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredand t
-  let mk_redand  ( ctx : context ) ( t : expr ) =
+  let mk_redor  ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredor t
-    expr_of_ptr ctx (Z3native.mk_bvredand (context_gno ctx) (Expr.gno t))
+  let mk_and  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvand t1 t2
-  let mk_redor  ( ctx : context ) ( t : expr ) =
+  let mk_or  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvor t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvredor (context_gno ctx) (Expr.gno t))
+  let mk_xor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxor t1 t2
-  let mk_and  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_nand  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnand t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_nor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnor t1 t2
-  let mk_or  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_xnor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxnor t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_neg  ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg t
-  let mk_xor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_add  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_sub  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub t1 t2
-  let mk_nand  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_mul  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_udiv  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvudiv t1 t2
-  let mk_nor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_sdiv  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_urem  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvurem t1 t2
-  let mk_xnor  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_srem  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsrem t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_smod  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsmod t1 t2
-  let mk_neg  ( ctx : context ) ( t : expr ) =
+  let mk_ult  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvult t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (Expr.gno t))
+  let mk_slt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvslt t1 t2
-  let mk_add  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_ule  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvule t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_sle  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsle t1 t2
-  let mk_sub  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_uge  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvuge t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_sge  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsge t1 t2
-  let mk_mul  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_ugt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvugt t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_sgt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsgt t1 t2
-  let mk_udiv  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_concat t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_sdiv  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_urem  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_srem  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_smod  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_ult  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))  
-  let mk_slt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
-  let mk_ule  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
-  let mk_sle  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
-  let mk_uge  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
-  let mk_sge  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
-  let mk_ugt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))               
-  let mk_sgt  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))               
-  let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
   let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : expr ) =
     expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (Expr.gno t))
   let mk_sign_ext  ( ctx : context ) ( i : int ) ( t : expr ) = 
@@ -1855,38 +1842,28 @@ struct
     expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (Expr.gno t))
   let mk_repeat  ( ctx : context ) ( i : int ) ( t : expr ) =
     expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (Expr.gno t))
-  let mk_shl  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_shl  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvshl t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (Expr.gno t1) (Expr.gno t2))       
+  let mk_lshr  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvlshr t1 t2
-  let mk_lshr  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_ashr  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvashr t1 t2
-    expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_ashr  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =    
-    expr_of_ptr ctx  (Z3native.mk_bvashr (context_gno ctx) (Expr.gno t1) (Expr.gno t2))  
   let mk_rotate_left  ( ctx : context ) ( i : int ) ( t : expr ) = 
     expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (Expr.gno t))
   let mk_rotate_right ( ctx : context ) ( i : int ) ( t : expr ) =
     expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (Expr.gno t))
-  let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_left t1 t2
-    expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_right t1 t2
-  let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (Expr.gno t1) (Expr.gno t2))       
   let mk_bv2int ( ctx : context ) ( t : expr ) ( signed : bool ) =
     expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (Expr.gno t) signed)
   let mk_add_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) =
     (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed))
-  let mk_add_no_underflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_add_no_underflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd_no_underflow t1 t2
-    (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))       
+  let mk_sub_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub_no_overflow t1 t2
-  let mk_sub_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))            
   let mk_sub_no_underflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) =
     (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed))
-  let mk_sdiv_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_sdiv_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv_no_overflow t1 t2
-    (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))
+  let mk_neg_no_overflow  ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg_no_overflow t
-  let mk_neg_no_overflow  ( ctx : context ) ( t : expr ) =
-    (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (Expr.gno t)))
   let mk_mul_no_overflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) =
     (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed))
-  let mk_mul_no_underflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_mul_no_underflow  ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul_no_underflow t1 t2
-    (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2)))       
   let mk_numeral ( ctx : context ) ( v : string ) ( size : int ) =
     expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx size)))
 end
@@ -1949,7 +1926,7 @@ struct
      (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative))
 
   let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) =
-     (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand)))
+     apply3 ctx Z3native.mk_fpa_fp sign exponent significand
   let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) =
      (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s)))
   let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) =
@@ -1997,54 +1974,30 @@ struct
   let mk_const_s ( ctx : context ) ( name : string ) ( s : Sort.sort ) =
     mk_const ctx (Symbol.mk_string ctx name) s
 
-  let mk_abs ( ctx : context ) ( t : expr ) =
+  let mk_abs ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_abs t
-    expr_of_ptr ctx (Z3native.mk_fpa_abs (context_gno ctx) (Expr.gno t))
+  let mk_neg ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_neg t
-  let mk_neg ( ctx : context ) ( t : expr ) =
+  let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_add rm t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_neg (context_gno ctx) (Expr.gno t))
+  let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_sub rm t1 t2
-  let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_mul rm t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_add (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
+  let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_div rm t1 t2
-  let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = apply4 ctx Z3native.mk_fpa_fma rm t1 t2 t3
-    expr_of_ptr ctx (Z3native.mk_fpa_sub (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
+  let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_sqrt rm t
-  let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_rem t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_mul (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
+  let mk_round_to_integral  ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_round_to_integral rm t
-  let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_min t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_div (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2))
+  let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_max t1 t2
-  let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) =
+  let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_leq t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_fma (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2) (Expr.gno t3))
+  let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =  apply2 ctx Z3native.mk_fpa_lt t1 t2
-  let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) =
+  let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_geq t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_sqrt (context_gno ctx) (Expr.gno rm) (Expr.gno t))
+  let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =  apply2 ctx Z3native.mk_fpa_gt t1 t2
-  let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =  apply2 ctx Z3native.mk_fpa_eq t1 t2
-    expr_of_ptr ctx (Z3native.mk_fpa_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_is_normal ( ctx : context ) ( t : expr ) =          apply1 ctx Z3native.mk_fpa_is_normal t
-  let mk_round_to_integral  ( ctx : context ) ( rm : expr ) ( t : expr ) =
+  let mk_is_subnormal ( ctx : context ) ( t : expr ) =       apply1 ctx Z3native.mk_fpa_is_subnormal t
-    expr_of_ptr ctx (Z3native.mk_fpa_round_to_integral (context_gno ctx) (Expr.gno rm) (Expr.gno t))
+  let mk_is_zero ( ctx : context ) ( t : expr ) =            apply1 ctx Z3native.mk_fpa_is_zero t
-  let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_is_infinite  ( ctx : context ) ( t : expr ) =       apply1 ctx Z3native.mk_fpa_is_infinite t
-    expr_of_ptr ctx (Z3native.mk_fpa_min (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_is_nan ( ctx : context ) ( t : expr ) =             apply1 ctx Z3native.mk_fpa_is_nan t
-  let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
+  let mk_is_negative  ( ctx : context ) ( t : expr ) =       apply1 ctx Z3native.mk_fpa_is_negative t
-    expr_of_ptr ctx (Z3native.mk_fpa_max (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
+  let mk_is_positive ( ctx : context ) ( t : expr ) =        apply1 ctx Z3native.mk_fpa_is_positive t
-  let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_leq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_geq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_eq (context_gno ctx) (Expr.gno t1) (Expr.gno t2))
-  let mk_is_normal ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_normal (context_gno ctx) (Expr.gno t))
-  let mk_is_subnormal ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_subnormal (context_gno ctx) (Expr.gno t))
-  let mk_is_zero ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_zero (context_gno ctx) (Expr.gno t))
-  let mk_is_infinite  ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_infinite (context_gno ctx) (Expr.gno t))
-  let mk_is_nan ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_nan (context_gno ctx) (Expr.gno t))
-  let mk_is_negative  ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t))
-  let mk_is_positive ( ctx : context ) ( t : expr ) =
-    expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t))
   let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s))
   let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) =
@@ -2059,8 +2012,7 @@ struct
     expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size)
   let mk_to_sbv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_sbv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size)
-  let mk_to_real ( ctx : context ) ( t : expr ) =
+  let mk_to_real ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_to_real t
-    expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t))
 
   let get_ebits ( ctx : context ) ( s : Sort.sort ) =
      (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s))

src/api/python/z3.py

@@ -3572,9 +3572,13 @@ def Concat(*args):
     if __debug__:
         _z3_assert(sz >= 2, "At least two arguments expected.")
 
-    ctx = args[0].ctx
+    ctx = None
-
+    for a in args:
-    if is_seq(args[0]):
+        if is_expr(a):
+            ctx = a.ctx
+            break
+    if is_seq(args[0]) or isinstance(args[0], str):
+        args = [_coerce_seq(s, ctx) for s in args]
         if __debug__:
             _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
         v = (Ast * sz)()
@@ -9066,7 +9070,12 @@ class SeqRef(ExprRef):
     def __add__(self, other):
         return Concat(self, other)
 
+    def __radd__(self, other):
+        return Concat(other, self)
+
     def __getitem__(self, i):
+        if _is_int(i):
+            i = IntVal(i, self.ctx)
         return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 
     def is_string(self):

src/muz/pdr/pdr_context.cpp

@@ -1705,6 +1705,7 @@ namespace pdr {
 
     void context::validate_search() {
         expr_ref tr = m_search.get_trace(*this);
+		TRACE("pdr", tout << tr << "\n";);
         smt::kernel solver(m, get_fparams());
         solver.assert_expr(tr);
         lbool res = solver.check();

src/smt/theory_arith_nl.h

@@ -354,6 +354,7 @@ namespace smt {
     */
     template<typename Ext>
     interval theory_arith<Ext>::evaluate_as_interval(expr * n) {
+        expr* arg;
         TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";);
         if (has_var(n)) {
             TRACE("nl_evaluate", tout << "n has a variable associated with it\n";);
@@ -385,6 +386,9 @@ namespace smt {
             TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";);
             return r;
         }
+        else if (m_util.is_to_real(n, arg)) {
+            return evaluate_as_interval(arg);
+        }
         else {
             rational val;
             if (m_util.is_numeral(n, val)) {
@@ -1660,7 +1664,7 @@ namespace smt {
                 3) (new non-int coeffs) This only happens in an optional step in the conversion. Now, for int rows, I only apply this optional step only if non-int coeffs are not created.
         */
 
-        if (is_mixed_real_integer(r))
+        if (!get_manager().int_real_coercions() && is_mixed_real_integer(r))
             return true; // giving up... see comment above
 
         TRACE("cross_nested", tout << "cheking problematic row...\n";);

src/smt/theory_bv.cpp

@@ -1178,29 +1178,35 @@ namespace smt {
             if (m_wpos[v] == idx)
                 find_wpos(v);            
 
-
             literal_vector & bits = m_bits[v];
             literal bit           = bits[idx];
             lbool   val           = ctx.get_assignment(bit); 
+            if (val == l_undef) {
+                continue;
+            }
             theory_var v2         = next(v);
             TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
+            literal antecedent = bit;
+
+            if (val == l_false) {
+                antecedent.neg();
+            }
             while (v2 != v) {
                 literal_vector & bits2   = m_bits[v2];
                 literal bit2             = bits2[idx];
                 SASSERT(bit != ~bit2);
                 lbool   val2             = ctx.get_assignment(bit2);
                 TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
+                
                 if (val != val2) {
-                    literal antecedent = bit;
                     literal consequent = bit2;
                     if (val == l_false) {
-                        antecedent.neg();
                         consequent.neg();
                     }
-                    SASSERT(ctx.get_assignment(antecedent) == l_true);
                     assign_bit(consequent, v, v2, idx, antecedent, false);
                     if (ctx.inconsistent()) {
                         TRACE("bv_bit_prop", tout << "inconsistent " << bit <<  " " << bit2 << "\n";);
+                        m_prop_queue.reset();
                         return;
                     }
                 }

src/smt/theory_seq.cpp

@@ -551,6 +551,9 @@ bool theory_seq::is_solved() {
         IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
         return false;
     }
+    if (!m_nqs.empty()) {
+        return false;
+    }
     for (unsigned i = 0; i < m_automata.size(); ++i) {
         if (!m_automata[i]) {
             IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
@@ -967,10 +970,10 @@ bool theory_seq::solve_ne(unsigned idx) {
         }
     }
 
+    bool updated = false;
     dependency* new_deps = n.dep();
     vector<expr_ref_vector> new_ls, new_rs;
     literal_vector new_lits(n.lits());
-    bool updated = false;
     for (unsigned i = 0; i < n.ls().size(); ++i) {
         expr_ref_vector& ls = m_ls;
         expr_ref_vector& rs = m_rs;
@@ -986,8 +989,7 @@ bool theory_seq::solve_ne(unsigned idx) {
             return true;
         }
         else if (!change) {
-//            std::cout << n.ls(i) << " " << ls << "\n";
+            TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";);
-//            std::cout << n.rs(i) << " " << rs << "\n";
             continue;
         }
         else {
@@ -1041,6 +1043,16 @@ bool theory_seq::solve_ne(unsigned idx) {
             new_deps = m_dm.mk_join(deps, new_deps);
         }
     }
+    if (!updated && num_undef_lits == 0) {
+        return false;
+    }
+    if (!updated) {
+        for (unsigned j = 0; j < n.ls().size(); ++j) {
+            new_ls.push_back(n.ls(j));
+            new_rs.push_back(n.rs(j));
+        }
+    }                                  
+
     if (num_undef_lits == 1 && new_ls.empty()) {
         literal_vector lits;
         literal undef_lit = null_literal;
@@ -1064,7 +1076,7 @@ bool theory_seq::solve_ne(unsigned idx) {
         propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); 
         return true;
     }
-    else if (updated) {
+    if (updated) {
         if (num_undef_lits == 0 && new_ls.empty()) {
             TRACE("seq", tout << "conflict\n";);
             set_conflict(new_deps, new_lits);