mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
6827 commits 23 branches 48 tags 157 MiB
Commit graph

6827 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6e6c5935d7 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-25 18:09:37 -08:00
Nikolaj Bjorner
777091e653 fix part 1 of #875 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:09:27 -08:00
Nikolaj Bjorner
4782e19086 fix bug in sat-simplifier decreasing heap values of variables that are not in the heap 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 16:21:51 -08:00
Nikolaj Bjorner
60783e5696 fix regression for z3num 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 13:26:58 -08:00
Nikolaj Bjorner
4ec4abd7e3 fix test for int-value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-23 13:31:43 -08:00
Murphy Berzish
09ac5645e4 parameterize theory-aware activity of overlap 2017-01-22 23:21:20 -05:00
Christoph M. Wintersteiger
adf8072eaa Added option to limit the distance of unsat core extension through patterns. 2017-01-21 12:28:37 +00:00
Murphy Berzish
50e2273dbd substr bugfix 2017-01-20 17:39:32 -05:00
Nikolaj Bjorner
1bfd09e16b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-19 19:31:24 -08:00
Nikolaj Bjorner
e23509797a access parameters from Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-19 19:28:20 -08:00
Christoph M. Wintersteiger
43d083bafb Windows build fix. 2017-01-19 11:19:29 +00:00
Christoph M. Wintersteiger
b9bfd4ddf5 Merge pull request #854 from angr/fix/fpic-arm 
Add -fpic to armv7/armv8 build
 2017-01-18 21:55:52 +00:00
Christoph M. Wintersteiger
5c1ffe13d1 x64 build fix for .NET 3.5 API 2017-01-18 13:06:28 +00:00
Christoph M. Wintersteiger
81c3a7dabd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-18 12:32:10 +00:00
Christoph M. Wintersteiger
a334020f2c Added .NET 3.5 solution/project files 2017-01-18 12:32:02 +00:00
Nikolaj Bjorner
16552d32cb Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 14:19:32 -08:00
Nikolaj Bjorner
0aa912371b Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 14:19:24 -08:00
Nikolaj Bjorner
735998c386 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-17 13:41:25 -08:00
Nikolaj Bjorner
873d975c77 fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-17 13:41:15 -08:00
Murphy Berzish
a570149b57 finite overlap models with binary search 2017-01-17 14:49:57 -05:00
Christoph M. Wintersteiger
6d34899c46 Bugfix for macro finder. Fixes #832. 2017-01-17 15:44:03 +00:00
Christoph M. Wintersteiger
0fae048e3e Windows build fix. 2017-01-17 12:58:32 +00:00
Murphy Berzish
794e210958 finite model fix 2017-01-16 21:42:11 -05:00
Murphy Berzish
0af834421f finite model finding for other concat cases in theory_str 2017-01-16 18:24:47 -05:00
Murphy Berzish
e459617c39 experimental finite model finding WIP, first successful run 2017-01-16 18:04:03 -05:00
Murphy Berzish
4e2847dea4 Revert "scale theory-aware priority by bvar_inc" 
This reverts commit aa8bf2668f.
 2017-01-16 15:46:28 -05:00
Murphy Berzish
4b6582b8f3 Revert "experimental z3str2 search order" 
This reverts commit 0dfaa30ae8.
 2017-01-16 15:46:17 -05:00
Murphy Berzish
0dfaa30ae8 experimental z3str2 search order 2017-01-16 14:46:04 -05:00
Christoph M. Wintersteiger
625681f82f Updated cmake build 2017-01-16 15:59:16 +00:00
Christoph M. Wintersteiger
e472a8d4cf Enabled filenames in error messages during inclusion of files. 2017-01-16 15:46:58 +00:00
Christoph M. Wintersteiger
090a331d79 Added filenames to error messages for when we have more than one file. 2017-01-16 15:43:13 +00:00
Christoph M. Wintersteiger
00a50eea7f Added (include ...) SMT2 command. 2017-01-16 15:05:58 +00:00
Christoph M. Wintersteiger
6fe1682378 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-16 14:08:26 +00:00
Christoph M. Wintersteiger
24e4f19d76 build fix 2017-01-16 14:08:21 +00:00
Nikolaj Bjorner
dc543a7ee7 update macro_util logging to uniform format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 21:13:22 -08:00
Nikolaj Bjorner
c4c9de0838 fix memory leaks from cancellations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 20:09:27 -08:00
Nikolaj Bjorner
24eae3f6e0 fix crash with unary xor #870 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 12:06:56 -08:00
Nikolaj Bjorner
dd0d3d4510 use stirngs for env variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:59:09 -08:00
Nikolaj Bjorner
ee36662435 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-15 11:56:01 -08:00
Nikolaj Bjorner
7df803c131 Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-15 11:52:48 -08:00
Murphy Berzish
aa8bf2668f scale theory-aware priority by bvar_inc 2017-01-14 15:28:58 -05:00
Murphy Berzish
a9ec8666f0 add phase selection to theory-aware branching queue 2017-01-14 14:43:57 -05:00
Christoph M. Wintersteiger
340ba7780e Added MAKEJOBS env var to mk_unix_dist.py 2017-01-14 18:57:10 +00:00
Christoph M. Wintersteiger
b30f3a6dbd Separated win32/64 builds 2017-01-14 14:56:25 +00:00
Christoph M. Wintersteiger
d8e4966a11 Added win64 build badge 2017-01-14 14:18:37 +00:00
Nikolaj Bjorner
bc6b3007de remove unused features related to weighted check-sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-13 20:53:22 -08:00
Christoph M. Wintersteiger
37916fe7e9 Update README.md 2017-01-13 21:33:11 +00:00
Christoph M. Wintersteiger
43eb6cc022 CI trigger 2017-01-13 20:43:53 +00:00
Murphy Berzish
dd03632f3d Merge branch 'develop' of github.com:mtrberzi/z3 into develop 2017-01-13 12:57:50 -05:00
Murphy Berzish
f033a77fae modify theory-aware branching to manipulate activity instead of giving absolute priority 2017-01-13 12:57:48 -05:00