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

azure-pipelines.yml

@@ -5,6 +5,7 @@ variables:
   cmakeNet: '-DZ3_BUILD_DOTNET_BINDINGS=True'
   cmakePy:  '-DZ3_BUILD_PYTHON_BINDINGS=True'
   cmakeStdArgs: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True -G "Ninja" ../'
+  cmakeCovArgs: '-DCMAKE_INSTALL_PREFIX=./install -G "Ninja" ../'
   asanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=address -fno-omit-frame-pointer" CFLAGS="${CFLAGS} -fsanitize=address -fno-omit-frame-pointer"'
   ubsanEnv: 'CXXFLAGS="${CXXFLAGS} -fsanitize=undefined" CFLAGS="${CFLAGS} -fsanitize=undefined"'
   msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"'
@@ -150,6 +151,30 @@ jobs:
     - ${{if eq(variables['runTests'], 'True')}}:
       - template: scripts/test-regressions.yml
 
+ 
+- job: "Ubuntu16CMakeCoverage"
+  displayName: "Ubuntu build - cmake w/ coverage"
+  pool:
+    vmImage: "ubuntu-latest"
+  steps:
+    - script: sudo apt-get install ninja-build 
+    - script: |
+        set -e
+        mkdir build
+        cd build
+        CXXFLAGS=--coverage LDFLAGS=-lgcov CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Debug $(cmakeCovArgs)
+        ninja
+        ninja test-z3
+        ninja install
+        cd ..
+    - script: |
+         cd build
+         ./test-z3 -a
+         cd ..
+    - template: scripts/test-examples-cmake.yml
+    - template: scripts/test-regressions-coverage.yml
+         
+
 - job: "WindowsLatest"
   displayName: "Windows"
   pool: 

examples/ml/README

@@ -14,9 +14,9 @@ for the byte-code version.
 If Z3 was installed into the ocamlfind package repository (see
 src/api/ml/README), then we can also compile this example as follows:  
 
-ocamlfind ocamlc -o ml_example.byte -package Z3 -linkpkg ml_example.ml
+ocamlfind ocamlc -o ml_example.byte -thread -package Z3 -linkpkg ml_example.ml
 or
-ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml
+ocamlfind ocamlopt -o ml_example -thread -package Z3 -linkpkg ml_example.ml
 
 Note that the resulting binaries depend on the shared z3 library
 (libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH

scripts/test-regressions-coverage.yaml

@@ -0,0 +1,4 @@
+steps:
+- script: git clone https://github.com/z3prover/z3test z3test
+- script: python z3test/scripts/test_benchmarks.py build/z3 z3test/regressions/smt2    
+- script: python z3test/scripts/test_coverage_tests.py build/install z3test/coverage/cpp    

src/ast/recfun_decl_plugin.cpp

@@ -338,7 +338,9 @@ namespace recfun {
 
 
     void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
-        expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs);        
+        expr_ref rhs1(rhs, m());
+        if (!is_macro)
+            rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs);        
         d.set_definition(subst, is_macro, n_vars, vars, rhs1);
     }
 

src/sat/tactic/goal2sat.cpp

@@ -544,6 +544,29 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
+    void convert_not(app* t, bool root, bool sign) {
+        SASSERT(t->get_num_args() == 1);
+        unsigned sz = m_result_stack.size();
+        SASSERT(sz >= 1);
+        sat::literal  lit = m_result_stack[sz - 1];
+        m_result_stack.shrink(sz - 1);
+        if (root) {
+            SASSERT(sz == 1);
+            mk_root_clause(sign ? lit : ~lit);            
+        }
+        else {
+            sat::bool_var k = add_var(false, t);
+            sat::literal  l(k, false);
+            cache(t, l);
+            // l <=> ~lit
+            mk_clause(lit, l);
+            mk_clause(~lit, ~l);
+            if (sign)
+                l.neg();
+            m_result_stack.push_back(l);
+        }
+    }
+
     void convert_implies(app* t, bool root, bool sign) {
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
@@ -702,6 +725,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
             case OP_IMPLIES:
                 convert_implies(t, root, sign);
                 break;
+            case OP_NOT:
+                convert_not(t, root, sign);
+                break;
             default:
                 UNREACHABLE();
             }
@@ -767,7 +793,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 m_frame_stack.pop_back();
                 continue;
             }
-            if (m.is_not(t)) {
+            if (m.is_not(t) && !m.is_not(t->get_arg(0))) {
                 m_frame_stack.pop_back();
                 visit(t->get_arg(0), root, !sign);
                 continue;