Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

.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

RELEASE_NOTES

@@ -14,6 +14,8 @@ Version 4.3.2
 
 - Removed 'autoconf' dependency. We do not need to execute 'autoconf' and './configure' anymore to build Z3.
 
+- Fixed incorrect result returned by Z3_solver_get_num_scopes. (Thanks to Herman Venter). This bug was introduced in Z3 4.3.0
+
 Version 4.3.1
 =============
 

examples/java/JavaExample.java

@@ -806,7 +806,6 @@ class JavaExample
     {
         System.out.println("BasicTests");
 
-        Symbol qi = ctx.MkSymbol(1);
         Symbol fname = ctx.MkSymbol("f");
         Symbol x = ctx.MkSymbol("x");
         Symbol y = ctx.MkSymbol("y");
@@ -2207,7 +2206,8 @@ class JavaExample
         } catch (Z3Exception ex)
         {
             System.out.println("Z3 Managed Exception: " + ex.getMessage());
-            System.out.println("Stack trace: " + ex.getStackTrace());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);            
         } catch (TestFailedException ex)
         {
             System.out.println("TEST CASE FAILED: " + ex.getMessage());

scripts/mk_util.py

@@ -985,7 +985,10 @@ class JavaDLLComponent(Component):
             else:
                 t = t.replace('PLATFORM', 'win32')
             out.write(t)
-            out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) Native$(OBJ_EXT) libz3$(LIB_EXT)\n')
+            if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
+                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(LIB_EXT)\n')
+            else:
+                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) api/java/Native$(OBJ_EXT) libz3$(SO_EXT)\n')
             out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
             # for java_file in get_java_files(self.src_dir):
             #     out.write('%s ' % java_file)

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,9 +524,27 @@ 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_Z3Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), java_method_name(name)))
+        java_wrapper.write('JNIEXPORT %s JNICALL Java_%s_Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
         i = 0;
         for param in params:
             java_wrapper.write(', ')
@@ -552,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)),
+                if param_type(param) == INT or param_type(param) == UINT:
-                                                                                             i,
+                    java_wrapper.write('  %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
-                                                                                             type2str(param_type(param)),
+                else:                    
-                                                                                             java_get_array_elements(param),
+                    java_wrapper.write('  GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, 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, 
@@ -601,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), 
+                if param_type(param) == INT or param_type(param) == UINT:
-                                                                                            i, 
+                    java_wrapper.write('  jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
-                                                                                            java_array_element_type(param),
+                else:
-                                                                                            i))
+                    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')

src/api/java/Context.java

@@ -2974,23 +2974,15 @@ public class Context extends IDisposable
 
 	void CheckContextMatch(Z3Object other) throws Z3Exception
 	{
-
+	    if (this != other.Context())
-		if (this == other.Context())
+		throw new Z3Exception("Context mismatch");
-			throw new Z3Exception("Context mismatch");
 	}
 
 	void CheckContextMatch(Z3Object[] arr) throws Z3Exception
 	{
-
+	    if (arr != null)
-		if (arr != null)
+		for (Z3Object a : arr)
-		{
+		    CheckContextMatch(a);
-			for (Z3Object a : arr)
-			{
-				// It was an assume, now we added the precondition, and we made
-				// it into an assert
-				CheckContextMatch(a);
-			}
-		}
 	}
 
 	private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
@@ -3091,8 +3083,6 @@ public class Context extends IDisposable
 	 **/
 	protected void finalize()
 	{
-		// Console.WriteLine("Context Finalizer from " +
-		// System.Threading.Thread.CurrentThread.ManagedThreadId);
 		Dispose();
 
 		if (m_refCount == 0)
@@ -3102,6 +3092,7 @@ public class Context extends IDisposable
 			m_ctx = 0;
 		} else
 			/* re-queue the finalizer */
+                        /* BUG: DRQ's need to be taken over too! */
 			new Context(m_ctx, m_refCount, m_n_err_handler);
 	}
 
@@ -3110,8 +3101,6 @@ public class Context extends IDisposable
 	 **/
 	public void Dispose()
 	{
-		// Console.WriteLine("Context Dispose from " +
-		// System.Threading.Thread.CurrentThread.ManagedThreadId);
 		m_AST_DRQ.Clear(this);
 		m_ASTMap_DRQ.Clear(this);
 		m_ASTVector_DRQ.Clear(this);

src/api/java/Z3Object.java

@@ -104,13 +104,12 @@ public class Z3Object extends IDisposable
             return null;
         long[] an = new long[a.length];
         for (int i = 0; i < a.length; i++)
-            if (a[i] != null)
+	    an[i] = a[i].NativeObject();
-                an[i] = a[i].NativeObject();
         return an;
     }
 
     static int ArrayLength(Z3Object[] a)
     {
-        return (a == null) ? 0 : (int) a.length;
+        return (a == null) ? 0 : a.length;
     }
 }

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);
 

src/solver/strategic_solver.cpp

@@ -308,7 +308,7 @@ void strategic_solver::pop(unsigned n) {
 unsigned strategic_solver::get_scope_level() const {
     if (m_ctx == 0)
         return 0;
-    return m_ctx->m_assertions.size();
+    return m_ctx->m_scopes.size();
 }
 
 struct aux_timeout_eh : public event_handler {