diff --git a/azure-pipelines.yml b/azure-pipelines.yml
index 60cf35dcd..59c012dd7 100644
--- a/azure-pipelines.yml
+++ b/azure-pipelines.yml
@@ -93,39 +93,42 @@ jobs:
 #   - template: scripts/test-jupyter.yml
 #   - template: scripts/test-java-cmake.yml
 #   - template: scripts/test-regressions.yml
-
-
+  
 - job: "LinuxCMake"
   displayName: "Ubuntu build - cmake"
   pool:
     vmImage: "Ubuntu-16.04"
   strategy:
     matrix:
-      debugClang:
-        cmdLine: 'CC=clang CXX=clang++ cmake $(cmakeStdArgs)'
-        runUnitTest: 'True'
       releaseClang:
-        cmdLine: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release $(cmakeStdArgs)'
-        runUnitTest: 'True'
+        setupCmd1: ''
+        setupCmd2: ''
+        buildCmd: 'CC=clang CXX=clang++ cmake -DCMAKE_BUILD_TYPE=Release $(cmakeStdArgs)'
+        runTests: 'True'
+      debugClang:
+        setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))"'
+        setupCmd2: 'JlCxxDir=$(julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))")'
+        buildCmd: 'CC=clang CXX=clang++ cmake -DJlCxx_DIR=$JlCxxDir/cmake/JlCxx -DZ3_BUILD_JULIA_BINDINGS=True $(cmakeStdArgs)'
+        runTests: 'True'
       debugGcc:
-        cmdLine: 'CC=gcc CXX=g++ cmake $(cmakeStdArgs)'
-        runUnitTest: 'True'
+        setupCmd1: ''
+        setupCmd2: ''
+        buildCmd: 'CC=gcc CXX=g++ cmake $(cmakeStdArgs)'
+        runTests: 'True'
       releaseSTGcc:
-        cmdLine: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DSINGLE_THREADED=ON $(cmakeStdArgs)'
-        runUnitTest: 'True'
-#      gccX86:
-#        cmdLine: 'CXXFLAGS="${CXXFLAGS} -m32" CFLAGS="${CFLAGS} -m32" CC=gcc-5 CXX=g++-5 cmake -DCMAKE_BUILD_TYPE=RelWithDebInfo $(cmakeStdArgs)'
-#        runUnitTest: 'True'
-#      asan:
-#        cmdLine: '$(asanEnv) cmake $(cmakeStdArgs)'
-#        runUnitTest: 'False'
+        setupCmd1: ''
+        setupCmd2: ''
+        buildCmd: 'CC=gcc CXX=g++ cmake -DCMAKE_BUILD_TYPE=Release -DSINGLE_THREADED=ON $(cmakeStdArgs)'
+        runTests: 'True'        
   steps:
     - script: sudo apt-get install ninja-build 
     - script: |
         set -e
         mkdir build
         cd build
-        $(cmdLine)
+        $(setupCmd1)
+        $(setupCmd2)
+        $(buildCmd)
         ninja
         ninja test-z3
         cd ..
@@ -133,27 +136,82 @@ jobs:
          cd build
          ./test-z3 -a
          cd ..
-      condition: eq(variables['runUnitTest'], 'True')
-    - template: scripts/test-examples-cmake.yml
+      condition: eq(variables['runTests'], 'True')
+    - ${{if eq(variables['runTests'], 'True')}}:
+      - template: scripts/test-examples-cmake.yml
 #   - template: scripts/test-jupyter.yml
 #   - template: scripts/test-java-cmake.yml
-    - template: scripts/test-regressions.yml
+    - ${{if eq(variables['runTests'], 'True')}}:
+      - template: scripts/test-regressions.yml
 
-
-- job: "Windows2017"
-  displayName: "Windows 2017 build"
-  pool:
-    vmImage: "vs2017-win2016"
+- job: "WindowsLatest"
+  displayName: "Windows Latest build"
+  pool: 
+    vmImage: "windows-latest"
+  strategy:
+    matrix:
+      x64:
+        arch: 'x64'
+        setupCmd1: ''
+        setupCmd2: ''
+        setupCmd3: ''
+        bindings: '-DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True'
+        runTests: 'True'
+      x86:
+        arch: 'x86'
+        setupCmd1: ''
+        setupCmd2: ''
+        setupCmd3: ''
+        bindings: '-DZ3_BUILD_PYTHON_BINDINGS=True'
+        runTests: 'False'
+      arm64:
+        arch: 'amd64_arm64'
+        setupCmd1: ''
+        setupCmd2: ''
+        setupCmd3: ''
+        bindings: ''
+        runTests: 'False'
+      Julia:
+        arch: 'x64'
+        setupCmd1: 'julia -e "using Pkg; Pkg.add(PackageSpec(name=\"libcxxwrap_julia_jll\", version=\"0.7.0\"))"'
+        setupCmd2: 'julia -e "using libcxxwrap_julia_jll; print(dirname(libcxxwrap_julia_jll.libcxxwrap_julia_path))" > tmp.env'
+        setupCmd3: 'set /P JlCxxDir=<tmp.env'
+        bindings:  '-DJlCxx_DIR=%JlCxxDir%\..\lib\cmake\JlCxx -DZ3_BUILD_JULIA_BINDINGS=True'
+        runTests:  'False'
   steps:
-    - script: scripts\vsts-vs2017.cmd x64
-
-- job: "Windows2017ARM64"
-  displayName: "Windows 2017 ARM64 build"
-  pool:
-    vmImage: "vs2017-win2016"
-  steps:
-    - script: scripts\vsts-vs2017.cmd amd64_arm64
+    - script: md build
+    - script: |
+         cd build
+         $(setupCmd1)
+         $(setupCmd2)
+         $(setupCmd3)
+         call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
+         cmake $(bindings) -G "NMake Makefiles" ../
+         nmake
+         cd ..
+    - script: |
+         call "C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" $(arch)
+         pushd build\python
+         python z3test.py z3
+         python z3test.py z3num
+         popd
+         pushd build
+         nmake cpp_example
+         examples\cpp_example_build_dir\cpp_example.exe
+         nmake c_example
+         examples\c_example_build_dir\c_example.exe
+         nmake java_example
+         nmake dotnet_example
+         nmake test-z3
+         test-z3.exe -a
+         popd
+      condition: eq(variables['runTests'], 'True')
+    - script: |
+         git clone https://github.com/z3prover/z3test z3test
+         python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
+      condition: eq(variables['runTests'], 'True')
 
+         
 - job: "MacOS"
   displayName: "MacOS build"
   pool:
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ac99fb294..fbeafee4d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -585,6 +585,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case _OP_STRING_STRIDOF: 
         UNREACHABLE();
     }
+    if (st == BR_FAILED) {
+        st = lift_ite(f, num_args, args, result);
+    }
     if (st != BR_FAILED && m().get_sort(result) != f->get_range()) {
         std::cout << expr_ref(m().mk_app(f, num_args, args), m()) << " -> " << result << "\n";
     }
@@ -685,21 +688,29 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_REWRITE2;
     }
-    expr* c = nullptr, *t = nullptr, *e = nullptr;
-    if (m().is_ite(a, c, t, e) && (t->get_ref_count() == 1 || e->get_ref_count() == 1)) {
-        result = m().mk_ite(c, m_util.str.mk_length(t), m_util.str.mk_length(e));
-        return BR_REWRITE3;
-    }
-#if 0
-    if (m().is_ite(a, c, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
-        result = m().mk_ite(c, m_util.str.mk_length(t), m_util.str.mk_length(e));
-        return BR_REWRITE3;
-    }
-#endif
-    
     return BR_FAILED;
 }
 
+br_status seq_rewriter::lift_ite(func_decl* f, unsigned n, expr* const* args, expr_ref& result) {
+    expr* c = nullptr, *t = nullptr, *e = nullptr;
+    for (unsigned i = 0; i < n; ++i) {        
+        if (m().is_ite(args[i], c, t, e) && 
+            (get_depth(t) <= 2 || t->get_ref_count() == 1 ||
+             get_depth(e) <= 2 || e->get_ref_count() == 1)) {
+            ptr_buffer<expr> new_args;
+            for (unsigned j = 0; j < n; ++j) new_args.push_back(args[j]);
+            new_args[i] = t;
+            expr_ref arg1(m().mk_app(f, new_args), m());
+            new_args[i] = e;
+            expr_ref arg2(m().mk_app(f, new_args), m());
+            result = m().mk_ite(c, arg1, arg2);
+            return BR_REWRITE2;
+        }
+    }
+    return BR_FAILED;
+}
+
+
 bool seq_rewriter::is_suffix(expr* s, expr* offset, expr* len) {
     expr_ref_vector lens(m());
     rational a, b;
@@ -771,21 +782,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool lengthPos   = m_util.str.is_length(b) || m_autil.is_add(b);
     sort* a_sort = m().get_sort(a);
 
-    expr* cond = nullptr, *t = nullptr, *e = nullptr;
-#if 0
-    if (m().is_ite(a, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
-        result = m().mk_ite(cond, m_util.str.mk_substr(t, b, c), m_util.str.mk_substr(e, b, c));
-        return BR_REWRITE3;
-    }
-    if (m().is_ite(b, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
-        result = m().mk_ite(cond, m_util.str.mk_substr(a, t, c), m_util.str.mk_substr(a, e, c));
-        return BR_REWRITE3;
-    }
-    if (m().is_ite(c, cond, t, e) && (get_depth(t) <= 2 || get_depth(e) <= 2)) {
-        result = m().mk_ite(cond, m_util.str.mk_substr(a, b, t), m_util.str.mk_substr(a, b, e));
-        return BR_REWRITE3;
-    }
-#endif
     sign sg;
     if (sign_is_determined(c, sg) && sg == sign_neg) {
         result = m_util.str.mk_empty(a_sort);
@@ -1759,6 +1755,7 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
         result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
         return BR_DONE;
     }
+    
     expr* c = nullptr, *t = nullptr, *e = nullptr;
     if (m().is_ite(a, c, t, e)) {
         result = m().mk_ite(c, m_util.str.mk_stoi(t), m_util.str.mk_stoi(e));
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index eaa788458..5a9e9283e 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -163,6 +163,7 @@ class seq_rewriter {
     br_status mk_re_opt(expr* a, expr_ref& result);
     br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result);
     br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
+    br_status lift_ite(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
 
     bool cannot_contain_prefix(expr* a, expr* b);
     bool cannot_contain_suffix(expr* a, expr* b);