diff --git a/.gitignore b/.gitignore
index d380fe06f..a26ee7565 100644
--- a/.gitignore
+++ b/.gitignore
@@ -34,6 +34,8 @@ ncscope.out
 # Commonly used directories for code
 bld_dbg/*
 bld_rel/*
+bld_dbg_x64/*
+bld_rel_x64/*
 # Auto generated files.
 config.log
 config.status
diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index db3cd30b2..75393378b 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -839,7 +839,7 @@ namespace test_mapi
             // Error handling test.
             try
             {
-                Expr plus_ri = ctx.MkAdd(ctx.MkInt(1), ctx.MkReal(2));
+                IntExpr i = ctx.MkInt("1/2");
                 throw new TestFailedException(); // unreachable
             }
             catch (Z3Exception)
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index d0bdcf8d4..7e403fecd 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -882,10 +882,10 @@ class JavaExample
         Expr inum = rn.Numerator();
         Expr iden = rn.Denominator();
         System.out.println("Numerator: " + inum + " Denominator: " + iden);
-        if (inum.toString() != "42" || iden.toString() != "43")
+        if (!inum.toString().equals("42") || !iden.toString().equals("43"))
             throw new TestFailedException();
 
-        if (rn.ToDecimalString(3) != "0.976?")
+        if (!rn.ToDecimalString(3).toString().equals("0.976?"))
             throw new TestFailedException();
 
         BigIntCheck(ctx, ctx.MkReal("-1231231232/234234333"));
@@ -895,23 +895,23 @@ class JavaExample
 
         String bn = "1234567890987654321";
 
-        if (ctx.MkInt(bn).BigInteger().toString() != bn)
+        if (!ctx.MkInt(bn).BigInteger().toString().equals(bn))
             throw new TestFailedException();
 
-        if (ctx.MkBV(bn, 128).BigInteger().toString() != bn)
+        if (!ctx.MkBV(bn, 128).BigInteger().toString().equals(bn))
             throw new TestFailedException();
 
-        if (ctx.MkBV(bn, 32).BigInteger().toString() == bn)
+        if (ctx.MkBV(bn, 32).BigInteger().toString().equals(bn))
             throw new TestFailedException();
 
         // Error handling test.
         try
         {
-            Expr plus_ri = ctx.MkAdd(new ArithExpr[] { ctx.MkInt(1),
-                    ctx.MkReal(2) });
+            IntExpr i = ctx.MkInt("0.5");
             throw new TestFailedException(); // unreachable
         } catch (Z3Exception e)
         {
+            System.out.println("GOT: " + e.getMessage());
         }
     }
 
@@ -2211,9 +2211,13 @@ class JavaExample
         } catch (TestFailedException ex)
         {
             System.out.println("TEST CASE FAILED: " + ex.getMessage());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);     
         } catch (Exception ex)
         {
             System.out.println("Unknown Exception: " + ex.getMessage());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);
         }
     }
 }
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 9167beceb..e55a3a356 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -468,18 +468,6 @@ def java_method_name(name):
         i = i + 1
     return result
 
-# Return the Java method name used to retrieve the elements of the given parameter
-def java_get_array_elements(p):
-    if param_type(p) == INT or param_type(p) == UINT:
-        return 'GetIntArrayElements'
-    else:
-        return 'GetLongArrayElements'
-# Return the Java method name used to release the elements of the given parameter
-def java_release_array_elements(p):
-    if param_type(p) == INT or param_type(p) == UINT:
-        return 'ReleaseIntArrayElements'
-    else:
-        return 'ReleaseLongArrayElements'
 # Return the type of the java array elements
 def java_array_element_type(p):
     if param_type(p) == INT or param_type(p) == UINT:
@@ -536,7 +524,24 @@ def mk_java():
     java_wrapper.write('#include"z3.h"\n')
     java_wrapper.write('#ifdef __cplusplus\n')
     java_wrapper.write('extern "C" {\n')
-    java_wrapper.write('#endif\n')
+    java_wrapper.write('#endif\n\n')
+    if VS_X64:        
+        java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW)                                   \\\n')
+        java_wrapper.write('  T * NEW = (T*) jenv->GetLongArrayElements(OLD, NULL);              \n')
+        java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW)                                 \\\n')
+        java_wrapper.write('  jenv->ReleaseLongArrayElements(OLD, (jlong *) NEW, JNI_ABORT);     \n\n')
+    else:
+        java_wrapper.write('#define GETLONGAELEMS(T,OLD,NEW)                                   \\\n')
+        java_wrapper.write('  T * NEW = 0; {                                                   \\\n')
+        java_wrapper.write('  jlong * temp = jenv->GetLongArrayElements(OLD, NULL);            \\\n')
+        java_wrapper.write('  unsigned int size = jenv->GetArrayLength(OLD);                   \\\n')
+        java_wrapper.write('  NEW = (T*) (new int[size]);                                      \\\n')
+        java_wrapper.write('  for (unsigned i=0; i < size; i++)                                \\\n')
+        java_wrapper.write('    NEW[i] = reinterpret_cast<T>(temp[i]);                         \\\n')
+        java_wrapper.write('  jenv->ReleaseLongArrayElements(OLD, temp, JNI_ABORT);            \\\n')
+        java_wrapper.write('  }                                                                  \n\n')
+        java_wrapper.write('#define RELEASELONGAELEMS(OLD,NEW)                                 \\\n')
+        java_wrapper.write('  delete [] NEW;                                                     \n\n')
     pkg_str = get_component('java').package_name.replace('.', '_')
     for name, result, params in _dotnet_decls:
         java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
@@ -553,11 +558,10 @@ def mk_java():
             if k == OUT or k == INOUT:
                 java_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
             elif k == IN_ARRAY or k == INOUT_ARRAY:
-                java_wrapper.write('  %s * _a%s = (%s *) jenv->%s(a%s, NULL);\n' % (type2str(param_type(param)),
-                                                                                             i,
-                                                                                             type2str(param_type(param)),
-                                                                                             java_get_array_elements(param),
-                                                                                             i))
+                if param_type(param) == INT or param_type(param) == UINT:
+                    java_wrapper.write('  %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
+                else:                    
+                    java_wrapper.write('  GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
             elif k == OUT_ARRAY:
                 java_wrapper.write('  %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), 
                                                                                                      i, 
@@ -602,10 +606,11 @@ def mk_java():
                                                                                                 i))
                 java_wrapper.write('  free(_a%s);\n' % i)
             elif k == IN_ARRAY or k == OUT_ARRAY:
-                java_wrapper.write('  jenv->%s(a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param), 
-                                                                                            i, 
-                                                                                            java_array_element_type(param),
-                                                                                            i))
+                if param_type(param) == INT or param_type(param) == UINT:
+                    java_wrapper.write('  jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
+                else:
+                    java_wrapper.write('  RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
+
             elif k == OUT or k == INOUT:
                 if param_type(param) == INT or param_type(param) == UINT:
                     java_wrapper.write('  {\n')
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 3e438d69d..ff36b4553 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -113,7 +113,6 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<BoolSort>() != null);
-
                 if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort;
             }
         }
@@ -134,7 +133,14 @@ namespace Microsoft.Z3
         /// <summary>
         /// Retrieves the Real sort of the context.
         /// </summary>
-        public RealSort RealSort { get { Contract.Ensures(Contract.Result<RealSort>() != null); if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; } }
+        public RealSort RealSort
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<RealSort>() != null); 
+                if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort;
+            }
+        }
 
         /// <summary>
         /// Create a new Boolean sort.
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index dade77eb1..9f5c04f0b 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -1532,8 +1532,7 @@ namespace Microsoft.Z3
                 {
                     case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
                     case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
-                    case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
-                    case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
+                    case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);                    
                 }
             }
 
@@ -1544,8 +1543,7 @@ namespace Microsoft.Z3
                 case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
                 case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
                 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
-                case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
-                case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort");
+                case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);                
             }
 
             return new Expr(ctx, obj);
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index b903f71e0..c3fbeab15 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -86,7 +86,6 @@ public class Context extends IDisposable
 	 **/
 	public BoolSort BoolSort() throws Z3Exception
 	{
-
 		if (m_boolSort == null)
 			m_boolSort = new BoolSort(this);
 		return m_boolSort;
@@ -97,7 +96,6 @@ public class Context extends IDisposable
 	 **/
 	public IntSort IntSort() throws Z3Exception
 	{
-
 		if (m_intSort == null)
 			m_intSort = new IntSort(this);
 		return m_intSort;
@@ -106,8 +104,10 @@ public class Context extends IDisposable
 	/**
 	 * Retrieves the Real sort of the context.
 	 **/
-	public RealSort RealSort()
+	public RealSort RealSort() throws Z3Exception 
 	{
+	    if (m_realSort== null)
+	        m_realSort = new RealSort(this);
 		return m_realSort;
 	}
 
diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java
index 88e67d82e..a67d94e7e 100644
--- a/src/api/java/Expr.java
+++ b/src/api/java/Expr.java
@@ -1786,8 +1786,6 @@ public class Expr extends AST
 				return new RatNum(ctx, obj);
 			case Z3_BV_SORT:
 				return new BitVecNum(ctx, obj);
-			case Z3_UNKNOWN_SORT:
-				throw new Z3Exception("Unknown Sort");
 			default: ;
 			}
 		}
@@ -1806,8 +1804,6 @@ public class Expr extends AST
 			return new ArrayExpr(ctx, obj);
 		case Z3_DATATYPE_SORT:
 			return new DatatypeExpr(ctx, obj);
-		case Z3_UNKNOWN_SORT:
-			throw new Z3Exception("Unknown Sort");
 		default: ;
 		}
 
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index f11c9852d..ec78f8e92 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -994,7 +994,7 @@ namespace datalog {
         p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
                       
         p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
-        p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
+        p.insert(":print-low-level-smt2", CPK_BOOL, "(default false) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
         
         PRIVATE_PARAMS(
             p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, 
@@ -1651,7 +1651,7 @@ namespace datalog {
         expr_ref_vector rules(m);
         svector<symbol> names;
         bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
-        bool print_low_level = m_params.get_bool(":print-low-level-smt2", true);
+        bool print_low_level = m_params.get_bool(":print-low-level-smt2", false);
 
 #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
 
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 798ee406d..2f43d518c 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -266,7 +266,7 @@ namespace pdr {
             }
             else if (is_invariant(tgt_level, curr, false, assumes_level)) {
                 
-                add_property(curr, tgt_level); // assumes_level?tgt_level:infty_level
+                add_property(curr, assumes_level?tgt_level:infty_level);
                 TRACE("pdr", tout << "is invariant: "<< tgt_level << " " << mk_pp(curr, m) << "\n";);              
                 src[i] = src.back();
                 src.pop_back();
@@ -293,9 +293,6 @@ namespace pdr {
 
     bool pred_transformer::add_property1(expr * lemma, unsigned lvl) {        
         if (is_infty_level(lvl)) {
-            if (m.is_false(lemma)) {
-                return false;
-            }
             if (!m_invariants.contains(lemma)) {
                 TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
                 m_invariants.push_back(lemma);
@@ -410,7 +407,7 @@ namespace pdr {
         add_property(result, level);        
     }
 
-    lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core) {
+    lbool pred_transformer::is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level) {
         TRACE("pdr", 
               tout << "is-reachable: " << head()->get_name() << " level: " << n.level() << "\n";
               tout << mk_pp(n.state(), m) << "\n";);
@@ -427,6 +424,9 @@ namespace pdr {
                   tout << mk_pp(n.state(), m) << "\n";);
             n.set_model(model);
         }
+        else if (is_sat == l_false) {
+            uses_level = m_solver.assumes_level();
+        }
         return is_sat;
     }
 
@@ -1640,7 +1640,8 @@ namespace pdr {
             close_node(n);
         }
         else {
-            switch (expand_state(n, cube)) {
+            bool uses_level = true;
+            switch (expand_state(n, cube, uses_level)) {
             case l_true:
                 if (n.level() == 0) {
                     TRACE("pdr", tout << "reachable\n";);
@@ -1653,7 +1654,7 @@ namespace pdr {
                 break;
             case l_false: {
                 core_generalizer::cores cores;
-                cores.push_back(std::make_pair(cube, true));
+                cores.push_back(std::make_pair(cube, uses_level));
                 
                 for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) {
                     core_generalizer::cores new_cores;                    
@@ -1666,7 +1667,7 @@ namespace pdr {
                 bool found_invariant = false;
                 for (unsigned i = 0; i < cores.size(); ++i) {
                     expr_ref_vector const& core = cores[i].first;
-                    bool uses_level = cores[i].second;
+                    uses_level = cores[i].second;
                     found_invariant = !uses_level || found_invariant;
                     expr_ref ncore(m_pm.mk_not_and(core), m);
                     TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") <<  mk_pp(ncore, m) << "\n";);
@@ -1690,8 +1691,8 @@ namespace pdr {
     // return a property that blocks state and is implied by the 
     // predicate transformer (or some unfolding of it).
     // 
-    lbool context::expand_state(model_node& n, expr_ref_vector& result) {
-        return n.pt().is_reachable(n, &result);
+    lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) {
+        return n.pt().is_reachable(n, &result, uses_level);
     }
 
     void context::propagate(unsigned max_prop_lvl) {    
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index c7f53752a..a201ac03b 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -140,7 +140,7 @@ namespace pdr {
         bool propagate_to_next_level(unsigned level);
         void add_property(expr * lemma, unsigned lvl);  // add property 'p' to state at level.
 
-        lbool is_reachable(model_node& n, expr_ref_vector* core);
+        lbool is_reachable(model_node& n, expr_ref_vector* core, bool& uses_level);
         bool is_invariant(unsigned level, expr* co_state, bool inductive, bool& assumes_level, expr_ref_vector* core = 0);
         bool check_inductive(unsigned level, expr_ref_vector& state, bool& assumes_level);
 
@@ -309,7 +309,7 @@ namespace pdr {
         void close_node(model_node& n);
         void check_pre_closed(model_node& n);
         void expand_node(model_node& n);
-        lbool expand_state(model_node& n, expr_ref_vector& cube);
+        lbool expand_state(model_node& n, expr_ref_vector& cube, bool& uses_level);
         void create_children(model_node& n);
         expr_ref mk_sat_answer() const;
         expr_ref mk_unsat_answer() const;