diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index efa3ec098..08a931fdc 100644
--- a/src/api/api_ast.cpp
+++ b/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;
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 8cb7670d7..dff2677df 100644
--- a/src/api/dotnet/Solver.cs
+++ b/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. 
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 356f933d4..b80ce3177 100644
--- a/src/api/z3_api.h
+++ b/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,