mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
10030 commits 49 branches 53 tags 182 MiB
Commit graph

10030 commits

This branch
This branch
All branches
Author SHA1 Message Date
Adrian Stanciu
45c60ed55c Update README.md 
Corrected path to Z3 Python interface
 2017-10-18 14:50:44 +03:00
Nikolaj Bjorner
8811d78415 compress elimination stack representation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 21:28:48 -07:00
Miguel Neves
cf2512ce90 Added literal promotion 2017-10-17 16:03:58 -07:00
Nikolaj Bjorner
e0e7836c12 working on BDD reordering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 14:20:49 -07:00
Nikolaj Bjorner
4944a86478 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-10-17 13:25:21 -07:00
Nikolaj Bjorner
43f8214453 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 13:25:08 -07:00
Nikolaj Bjorner
f39a4ece0d Merge pull request #6 from TheRealNebus/opt 
Lookahead clause size optimization. Fixed some missing propagations
 2017-10-17 13:22:40 -07:00
Miguel Neves
806690571e Lookahead clause size optimization. Fixed some missing propagations 2017-10-17 13:15:34 -07:00
Nikolaj Bjorner
7f590b5419 gift for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:27:58 -07:00
Nikolaj Bjorner
448cf8c31d fix scope accounting for dom simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 10:14:26 -07:00
Nikolaj Bjorner
42e9a0156b add elimination stack for model reconstruction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-17 04:52:06 -07:00
Nikolaj Bjorner
da4e8118b2 adding elim sequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 17:58:56 -07:00
Nuno Lopes
4e92caa553 nnf: let's try a different version of compatible frames wo/ copying 2017-10-16 22:33:23 +01:00
Christoph M. Wintersteiger
01f642a6f3 Backward compatibility 2017-10-16 18:19:55 +01:00
Nikolaj Bjorner
019edcb822 frame, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:35:00 -07:00
Nikolaj Bjorner
5f9891c235 moving out construction of expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:29:26 -07:00
Nikolaj Bjorner
a93f1f88cc trying to fix mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:23:50 -07:00
Nikolaj Bjorner
256c9d76d3 add macro for _Exit under WINDOWS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:14:10 -07:00
Nikolaj Bjorner
b36f512879 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 09:07:44 -07:00
Christoph M. Wintersteiger
a10ad79f2b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 17:07:10 +01:00
Christoph M. Wintersteiger
f9adf8e62a Backwards compatibility 2017-10-16 17:07:03 +01:00
Nikolaj Bjorner
d9ccb3928e fix debug build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-16 09:05:25 -07:00
Christoph M. Wintersteiger
cda03b4238 Whitespace 2017-10-16 17:01:09 +01:00
Nikolaj Bjorner
6327bd2c08 Merge pull request #1289 from delcypher/travis_ci_enable_asan_ubsan_build 
[TravisCI] Enable UBSan and ASan configurations
 2017-10-16 08:54:25 -07:00
Christoph M. Wintersteiger
0169417c64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-16 16:40:39 +01:00
Dan Liew
7c99721b60 [TravisCI] Don't run Python regression tests under ASan for now. 
The script that runs them doesn't propagate LD_PRELOAD and so the
tests fail.
 2017-10-16 13:21:03 +01:00
Dan Liew
a1b6316e2e [TravisCI] Try to unbreak running Python regression tests under ASan. 2017-10-16 09:49:54 +01:00
Dan Liew
8835b54d16 [TravisCI] Add ASan/UBSan configuration that runs unit tests. 2017-10-16 08:56:17 +01:00
Dan Liew
88fb31ac08 [TravisCI] Add RUN_API_EXAMPLES option so that we can disable 
building/running examples in some configurations.
 2017-10-16 08:56:17 +01:00
Dan Liew
dbb7f616c1 More LSan workarounds. 2017-10-16 08:56:17 +01:00
Dan Liew
e51ce8bcaf [TravisCI] Try again to not show suppressions by default 2017-10-16 08:56:17 +01:00
Dan Liew
ead6e56d15 [TravisCI] Swap run_quiet and run_non_native_binding. In the 
previous order `grep` inside `run_quiet` would get ASan LD_PRELOAD'ed
which would sometimes fail.
 2017-10-16 08:56:17 +01:00
Dan Liew
ecadef6e48 [TravisCI] Try to fix case in run_quiet where the script would fail 
with.

```
-ne: unary operator expected
```
 2017-10-16 08:56:17 +01:00
Dan Liew
ad2a0a0085 [TravisCI] Don't print sanitizer suppressions by default because 
that breaks Z3's regression tests.
 2017-10-16 08:56:17 +01:00
Dan Liew
35f6746c60 Workaround regressions/smt2/error.smt2 test timing out. 
When ASan's LeakSanitizer is enabled leak checking is triggered
when `exit()` is called and it returns so many false positives that
it takes a long time to write them to the console.

To workaround this we simply call `_Exit()` instead.
 2017-10-16 08:56:17 +01:00
Dan Liew
fd98593a58 [ASan] Ignore Clang OpenMP leaks for now. 2017-10-16 08:56:17 +01:00
Dan Liew
2dd1a4046d [TravisCI] Fix typo 2017-10-16 08:56:17 +01:00
Dan Liew
fd391e75a6 [TravisCI] Fix Z3_BUILD_TYPE variable that was not propagated 
into the Docker image as an environment variable.
 2017-10-16 08:56:17 +01:00
Dan Liew
675a3ae9dd [UBSan] Remove a bunch of suppressions. 2017-10-16 08:56:17 +01:00
Dan Liew
db7b2e989d [TravisCI] Try to run the Python and .NET examples under ASan. 2017-10-16 08:56:17 +01:00
Dan Liew
8d600050db [LSan] Remove suppression files. The were fixed on rebase 2017-10-16 08:56:17 +01:00
Dan Liew
ff5df20deb [LSan] Don't run c_maxsat_example with LeakSanitizer because 
it contains leaks that the Z3 developers don't intend to fix.
 2017-10-16 08:56:17 +01:00
Dan Liew
f90fe928af [LSan] Suppress another leak until I can figure out what is going on. 2017-10-16 08:56:17 +01:00
Dan Liew
bcff86a316 [LSan] Add suppression for part of #1297. 2017-10-16 08:56:17 +01:00
Dan Liew
a991e44a25 [TravisCI] Fix typo in created directory for suppression files 2017-10-16 08:56:17 +01:00
Dan Liew
5bcdea1ae5 [TravisCI] For ASan/LSan use larger context so we get larger stack 
traces if needed.
 2017-10-16 08:56:17 +01:00
Dan Liew
38d9e2df84 [TravisCI] Make ASan/UBSan configuration a debug build. 2017-10-16 08:56:17 +01:00
Dan Liew
11f7298c52 [TravisCI] Add ASan configuration 2017-10-16 08:56:17 +01:00
Dan Liew
157c8064e8 [CMake] When building C/C++ API examples use the same build type 
as Z3 if doing a single configuration build.
 2017-10-16 08:56:17 +01:00
Dan Liew
4db5980a23 [TravisCI] Fix getting proper stack traces for ASan/LSan. The 
`llvm-symbolizer` tool needs to be installed and ASan/LSan needs
to be told where to find it.
 2017-10-16 08:56:17 +01:00