From 5fe0eeda6334b53b2f281065849135fc9912aec7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 May 2020 09:36:42 -0700 Subject: [PATCH] disable regressions in ST mode Signed-off-by: Nikolaj Bjorner --- azure-pipelines.yml | 5 ++++- scripts/test-examples-cmake.yml | 2 +- src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index 42b4c0859..e3afa4ef7 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -26,8 +26,10 @@ jobs: matrix: MT: cmdLine: 'python scripts/mk_make.py -d --java --dotnet' + runRegressions: 'True' ST: cmdLine: './configure --single-threaded' + runRegressions: 'False' steps: - script: $(cmdLine) - script: | @@ -38,7 +40,8 @@ jobs: make -j3 test-z3 cd .. - template: scripts/test-z3.yml - - template: scripts/test-regressions.yml + - ${{if eq(variables['runRegressions'], 'True')}}: + - template: scripts/test-regressions.yml - template: scripts/generate-doc.yml - job: "Ubuntu18Python" diff --git a/scripts/test-examples-cmake.yml b/scripts/test-examples-cmake.yml index 97c35e3e4..f47e4c7e8 100644 --- a/scripts/test-examples-cmake.yml +++ b/scripts/test-examples-cmake.yml @@ -9,7 +9,7 @@ steps: examples/c_example_build_dir/c_example examples/cpp_example_build_dir/cpp_example examples/tptp_build_dir/z3_tptp5 -help + echo examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt cd .. -# examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6e5da2d01..68a0d83bc 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2010,8 +2010,8 @@ expr_ref seq_rewriter::is_nullable(expr* r) { result = mk_or(m(), is_nullable(r1), is_nullable(r2)); } else if (m_util.re.is_diff(r, r1, r2)) { - expr_ref e2(mk_not(m(), is_nullable(r2)), m()); - result = mk_and(m(), is_nullable(r1), e2); + result = mk_not(m(), is_nullable(r2)); + result = mk_and(m(), is_nullable(r1), result); } else if (m_util.re.is_star(r) || m_util.re.is_opt(r) ||