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

src/api/api_ast.cpp

@@ -1063,9 +1063,10 @@ extern "C" {
             case OP_BV2INT:    return Z3_OP_BV2INT;
             case OP_CARRY:     return Z3_OP_CARRY;
             case OP_XOR3:      return Z3_OP_XOR3;
+            case OP_BIT2BOOL: return Z3_OP_BIT2BOOL;
             case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL;
             case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL;
-            case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;
+            case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL;                
             case OP_BSDIV_I: return Z3_OP_BSDIV_I;
             case OP_BUDIV_I: return Z3_OP_BUDIV_I;
             case OP_BSREM_I: return Z3_OP_BSREM_I;

src/api/dotnet/Solver.cs

@@ -18,6 +18,7 @@ Notes:
 --*/
 
 using System;
+using System.Linq;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
@@ -126,6 +127,14 @@ namespace Microsoft.Z3
             Assert(constraints);
         }
 
+        /// <summary>
+        /// Alias for Assert.
+        /// </summary>        
+        public void Add(IEnumerable<BoolExpr> constraints)
+        {
+            Assert(constraints.ToArray());
+        }
+
         /// <summary>
         /// Assert multiple constraints into the solver, and track them (in the unsat) core 
         /// using the Boolean constants in ps. 

src/api/z3_api.h

@@ -1060,6 +1060,7 @@ typedef enum {
     Z3_OP_EXT_ROTATE_LEFT,
     Z3_OP_EXT_ROTATE_RIGHT,
 
+    Z3_OP_BIT2BOOL,
     Z3_OP_INT2BV,
     Z3_OP_BV2INT,
     Z3_OP_CARRY,

src/sat/sat_config.cpp

@@ -23,10 +23,10 @@ Revision History:
 namespace sat {
 
     config::config(params_ref const & p):
+        m_restart_max(0),
         m_always_true("always_true"),
         m_always_false("always_false"),
         m_caching("caching"),
-        m_restart_max(0),
         m_random("random"),
         m_geometric("geometric"),
         m_luby("luby"),