diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 2085de296..4361cab96 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -474,7 +474,7 @@ namespace test_mapi
                 cells_c[i] = new BoolExpr[9];
                 for (uint j = 0; j < 9; j++)
                     cells_c[i][j] = ctx.MkAnd(ctx.MkLe(ctx.MkInt(1), X[i][j]),
-                                                ctx.MkLe(X[i][j], ctx.MkInt(9)));
+                                              ctx.MkLe(X[i][j], ctx.MkInt(9)));
             }
 
             // each row contains a digit at most once
@@ -485,7 +485,13 @@ namespace test_mapi
             // each column contains a digit at most once
             BoolExpr[] cols_c = new BoolExpr[9];
             for (uint j = 0; j < 9; j++)
-                cols_c[j] = ctx.MkDistinct(X[j]);
+            {
+                IntExpr[] column = new IntExpr[9];
+                for (uint i = 0; i < 9; i++)
+                    column[i] = X[i][j];
+
+                cols_c[j] = ctx.MkDistinct(column);
+            }
 
             // each 3x3 square contains a digit at most once
             BoolExpr[][] sq_c = new BoolExpr[3][];
@@ -2087,7 +2093,7 @@ namespace test_mapi
                 {
                     QuantifierExample3(ctx);
                     QuantifierExample4(ctx);
-                }                
+                }
 
                 Log.Close();
                 if (Log.isOpen())
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a255c2d97..6f745d620 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1305,7 +1305,7 @@ namespace z3 {
         expr as_expr() const {
             unsigned n = size();
             if (n == 0) 
-                return ctx().bool_val(false);
+                return ctx().bool_val(true);
             else if (n == 1)
                 return operator[](0);
             else {
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 8b77244f9..f1c61619a 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -210,6 +210,10 @@ func_decl * bv_decl_plugin::mk_unary(ptr_vector<func_decl> & decls, decl_kind k,
 
 func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters, parameter const * parameters,
                                     unsigned arity, sort * const * domain) {
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
+
     force_ptr_array_size(m_int2bv, bv_size + 1);
 
     if (arity != 1) {
@@ -415,6 +419,9 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
         return 0;
     }
     unsigned bv_size = parameters[1].get_int();
+    if (bv_size == 0) {
+        m_manager->raise_exception("bit-vector size must be greater than zero");
+    }
     // TODO: sign an error if the parameters[0] is out of range, that is, it is a value not in [0, 2^{bv_size})
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index 234c343b8..ff24d1ceb 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -2437,7 +2437,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     t = m_bv_util.mk_bv_sub(t, lz); 
     t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min));
     expr_ref TINY(m);
-    TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2));
+    TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2));
     
     TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;);
     SASSERT(is_well_sorted(m, TINY));
@@ -2481,7 +2481,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
     dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
     dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
-    sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size));
+    sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size));
     dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero);
 
     sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size));