mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

disable regressions in ST mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-19 09:36:42 -07:00
parent 232f1b5fbe
commit 5fe0eeda63
3 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
azure-pipelines.yml
View file

@ -26,8 +26,10 @@ jobs:
matrix: matrix:
MT: MT:
cmdLine: 'python scripts/mk_make.py -d --java --dotnet' cmdLine: 'python scripts/mk_make.py -d --java --dotnet'
runRegressions: 'True'
ST: ST:
cmdLine: './configure --single-threaded' cmdLine: './configure --single-threaded'
runRegressions: 'False'
steps: steps:
- script: $(cmdLine) - script: $(cmdLine)
- script: | - script: |
@ -38,6 +40,7 @@ jobs:
make -j3 test-z3 make -j3 test-z3
cd .. cd ..
- template: scripts/test-z3.yml - template: scripts/test-z3.yml
- ${{if eq(variables['runRegressions'], 'True')}}:
- template: scripts/test-regressions.yml - template: scripts/test-regressions.yml
- template: scripts/generate-doc.yml - template: scripts/generate-doc.yml

2
scripts/test-examples-cmake.yml
View file

@ -9,7 +9,7 @@ steps:
examples/c_example_build_dir/c_example examples/c_example_build_dir/c_example
examples/cpp_example_build_dir/cpp_example examples/cpp_example_build_dir/cpp_example
examples/tptp_build_dir/z3_tptp5 -help examples/tptp_build_dir/z3_tptp5 -help
echo examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt
cd .. cd ..
# examples/c_maxsat_example_build_dir/c_maxsat_example ../examples/maxsat/ex.smt

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -2010,8 +2010,8 @@ expr_ref seq_rewriter::is_nullable(expr* r) {
result = mk_or(m(), is_nullable(r1), is_nullable(r2)); result = mk_or(m(), is_nullable(r1), is_nullable(r2));
} }
else if (m_util.re.is_diff(r, r1, r2)) { else if (m_util.re.is_diff(r, r1, r2)) {
expr_ref e2(mk_not(m(), is_nullable(r2)), m()); result = mk_not(m(), is_nullable(r2));
result = mk_and(m(), is_nullable(r1), e2); result = mk_and(m(), is_nullable(r1), result);
} }
else if (m_util.re.is_star(r) || else if (m_util.re.is_star(r) ||
m_util.re.is_opt(r) || m_util.re.is_opt(r) ||