mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
6742 commits 49 branches 53 tags 182 MiB
Commit graph

6742 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
af0ea13570 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-30 11:30:52 -08:00
Nikolaj Bjorner
76bc4f0b38 refine parsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 11:30:42 -08:00
Christoph M. Wintersteiger
841b5be40b Merge pull request #885 from martin-neuhaeusser/master 
Fix off-by-one bug in array indexing in the OCaml bindings
 2017-01-30 17:58:42 +00:00
martin-neuhaeusser
0e966f21ff Fix off-by-one bug in array indexing in the OCaml bindings 
This patch fixes an off-by-one bug that occurred in the construction of output arrays
in the OCaml bindings.
 2017-01-30 17:28:24 +01:00
Nikolaj Bjorner
dadcc6e8ff Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-30 02:09:26 -08:00
Nikolaj Bjorner
37ee4c95c3 adding parallel threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 02:09:08 -08:00
Murphy Berzish
fa1ec0b80f smtlib25 draft standard in theory_str 2017-01-27 16:49:40 -05:00
Murphy Berzish
a879b24011 add str.prefixof, str.suffixof in theory_str 2017-01-27 16:26:30 -05:00
Doug Woos
a9d61d48ae Add basic Sine Qua Non filtering 2017-01-27 11:22:39 -08:00
Doug Woos
5796e15088 Thread labels through tactic system 2017-01-27 11:07:13 -08:00
Nikolaj Bjorner
b70f1f0319 fix overflow exposed in #880 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-27 09:47:18 -08:00
Nikolaj Bjorner
962979b09c rework sat.mus to use restart count for bounded minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 13:28:40 -08:00
Nikolaj Bjorner
c3eb279637 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-01-26 08:37:54 -08:00
Nikolaj Bjorner
a0a81fc2d7 add format #879 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-26 08:37:37 -08:00
Nikolaj Bjorner
7386e2f3e9 add warning for scearios of #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-25 18:29:30 -08:00
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