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

8173 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b5100b5b6a Merge branch 'master' of https://github.com/z3prover/z3 2018-05-22 20:02:16 -07:00
Nikolaj Bjorner
363d7aad2a fix bug reported in #1637 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 20:02:08 -07:00
Nikolaj Bjorner
f2aae7cffa release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 16:59:11 -07:00
Nikolaj Bjorner
3b1b82bef0 bumping version number by 1 for release tagging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 10:19:38 -07:00
Nikolaj Bjorner
c390b72e42
Merge pull request #1635 from danielschemmel/cmake-cpp11 
Use CMake's own mechanism for selecting language version
 2018-05-21 08:46:01 -07:00
Daniel Schemmel
7467368266
Use CMake's own mechanism for selecting language version if CMake version is new enough 2018-05-21 07:35:43 +02:00
Nikolaj Bjorner
6938c76950
Merge pull request #1630 from danielschemmel/warnings 
Fix GCC Warnings
 2018-05-20 10:24:05 -07:00
Daniel Schemmel
78087483ca
Add missing include 
The code should not have compiled previously, as smt::context was only forward declared at this point.
 2018-05-20 15:34:01 +02:00
Daniel Schemmel
9c5a0ee810
Remove unnecessary (and confusing) parantheses around variable name in its declaration. 
Also fixes GCC warning [-Wparentheses].
 2018-05-20 15:34:01 +02:00
Nikolaj Bjorner
470e49afc1
Merge pull request #1631 from JoranHonig/master 
Parallel python example
 2018-05-19 11:08:23 -07:00
Joran Honig
e32dfad81e Add comments 2018-05-19 11:16:20 +02:00
Joran Honig
7d51353b8b Implement parallel python example 2018-05-19 11:13:53 +02:00
Daniel Schemmel
f02d031d11
As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value 2018-05-19 04:39:36 +02:00
Daniel Schemmel
5134c16833
NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized 2018-05-19 03:45:05 +02:00
Daniel Schemmel
1cc4a4ccc5
remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized 2018-05-19 02:56:46 +02:00
Nikolaj Bjorner
ad973d5c6d Merge branch 'master' of https://github.com/z3prover/z3 2018-05-18 14:31:16 -07:00
Nikolaj Bjorner
4b3483ec6e Merge branch 'master' of https://github.com/z3prover/z3 2018-05-18 14:30:35 -07:00
Nikolaj Bjorner
d462ed3f00 fix #1621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-18 14:30:27 -07:00
Nikolaj Bjorner
8302360321 fix #1625 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-18 14:24:12 -07:00
Nikolaj Bjorner
925867dc3e fix #1621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-18 14:14:00 -07:00
Nikolaj Bjorner
e5b14ab682 fix #1625 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-18 14:03:32 -07:00
Nikolaj Bjorner
2c71640503
Merge pull request #1624 from sb98052/master 
Link in Big_int via num package
 2018-05-17 20:58:30 -07:00
Sapan Bhatia
c198b12743 Big_int is no longer a part of OCaml's standard library and must be 
included via the num package: https://github.com/ocaml/num
 2018-05-15 04:55:57 +05:30
Nikolaj Bjorner
a6829ea9d0 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-13 05:40:56 -07:00
Nikolaj Bjorner
53976d0ddf
Merge pull request #1613 from corrodedHash/master 
Fixed Segfault when failing to load datalog file
 2018-05-08 18:55:35 +01:00
corrodedHash
d097d90731 Fixed Segfault when failing to load datalog file 2018-05-08 19:26:14 +02:00
Nikolaj Bjorner
bc3719f436
Merge pull request #1612 from danielschemmel/gcc8 
`lp::permutation_matrix::values` attempts an incorrect conversion
 2018-05-08 15:49:22 +01:00
Daniel Schemmel
2d5dd80238
The Permutation Matrix' values function attempted an incorrect conversion. 
This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE.
 2018-05-07 23:33:40 +02:00
Nikolaj Bjorner
502d0e37dd
Merge pull request #1611 from Z3Prover/revert-1610-cv/encoding 
Revert "Specify encoding of source files in mk_util.py"
 2018-05-03 12:00:03 -07:00
Nikolaj Bjorner
888699548d
Revert "Specify encoding of source files in mk_util.py" 2018-05-03 11:59:49 -07:00
Nikolaj Bjorner
c293d325a9
Merge pull request #1610 from varming/cv/encoding 
Specify encoding of source files in mk_util.py
 2018-05-03 11:51:37 -07:00
Nikolaj Bjorner
6e03c7a542 fix #1607 by filtering exceptions when the context is canceled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 03:23:54 -07:00
Carsten Varming
c279fd9f2e Specify encoding of source files in mk_util.py 2018-05-02 23:27:33 -04:00
Nikolaj Bjorner
6bff15e12e fix #1609 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-02 10:38:46 -07:00
Nikolaj Bjorner
fd5159bf18 Merge branch 'master' of https://github.com/z3prover/z3 2018-05-01 07:13:05 -07:00
Nikolaj Bjorner
371880da04 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 07:13:03 -07:00
Nikolaj Bjorner
b8193a0ae6 fix #1604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-29 10:04:42 -07:00
Nikolaj Bjorner
c64d044e60 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-27 17:49:51 +02:00
Nikolaj Bjorner
f234bb348b fix #1599. fix #1600 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-27 17:49:20 +02:00
Nikolaj Bjorner
5dbba8bd53 fix #1599. fix #1600 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-27 17:48:04 +02:00
Nikolaj Bjorner
a9568d1b12
Merge pull request #1597 from TheRealNebus/master 
WMax Bug Fix
 2018-04-27 09:53:29 +02:00
Nikolaj Bjorner
b5c77065e9
Merge pull request #1596 from mtrberzi/develop 
fix memory leak related to #1575
 2018-04-27 09:52:50 +02:00
TheRealNebus
24b35fb925 WMax conflict budget bug fix 2018-04-26 22:42:55 +01:00
TheRealNebus
e1d7f5deba Revert "MSS based MaxSMT solver" 
This reverts commit 3bbc09c1d2.
 2018-04-26 22:40:00 +01:00
TheRealNebus
7e8ed0762d Revert "implemented CLD" 
This reverts commit 3a7efb91ae.
 2018-04-26 22:39:58 +01:00
TheRealNebus
bf2a031f7b Revert "disjoint cores" 
This reverts commit e5aa79ba6a.
 2018-04-26 22:39:55 +01:00
TheRealNebus
37852807b0 Revert "WMax conflict budget bug fix" 
This reverts commit ab8d3cdc44.
 2018-04-26 22:39:45 +01:00
Murphy Berzish
047f6c558c fix memory leak related to #1575 2018-04-26 16:36:14 -04:00
Nikolaj Bjorner
74292a48e5 change order of concatentation for empty string, #1595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-26 09:08:34 +02:00
Nikolaj Bjorner
a04921dafe fix #1595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-26 08:47:05 +02:00