mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
8153 commits 23 branches 48 tags 156 MiB
Commit graph

8153 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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 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 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 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
Nikolaj Bjorner cf2258a536 fix #1594 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-26 08:39:35 +02:00
Nikolaj Bjorner f54779fe09 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-25 11:18:39 +02:00
Nikolaj Bjorner b5f067bec5 fix #1592 #1587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-25 11:18:24 +02:00
TheRealNebus ab8d3cdc44 WMax conflict budget bug fix 2018-04-24 17:59:21 +01:00
Nikolaj Bjorner 484d20c1f2
Merge pull request #1591 from yxliang01/master 
Z3 now will also try to find libz3 in PYTHONPATH
 2018-04-24 17:23:27 +02:00
yxliang01 f7bcf0fd58 Z3 now will also try to find libz3 in PYTHONPATH 2018-04-24 08:17:20 -07:00
Christoph M. Wintersteiger e13f3d92af Updated CMakelists.txt 2018-04-24 15:01:05 +01:00
Christoph M. Wintersteiger 2e3c335e14 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-04-24 12:43:14 +01:00
Christoph M. Wintersteiger a1d870f19f Added tactic for QF_FPLRA 2018-04-24 12:43:11 +01:00
Nikolaj Bjorner e3a40459bf
Merge pull request #1588 from bannsec/z3_nonascii_encoding 
Fancy dots are not allowed here!!
 2018-04-24 08:34:50 +02:00
bannsec 5166b96d20 Fancy dots are not allowed here!! 2018-04-23 17:17:51 -04:00
Nikolaj Bjorner 19bb883263 fix #1581 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 12:12:39 +02:00
Nikolaj Bjorner 480e1c4dab add warning message for optimization with quantifiers. Fix #1580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:20:24 +02:00
Nikolaj Bjorner 0b4e54be38 fix #1583 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:15:04 +02:00
Nikolaj Bjorner 279f1986a6 fix #1575, fix #1585 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-23 07:11:15 +02:00
Nikolaj Bjorner f22abaa713 enable patterns on equality, add trace for variables for axiom profiling. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-20 11:44:30 +03:00
Nikolaj Bjorner b79440a21d add web assembly link 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 21:13:24 -07:00
Nikolaj Bjorner 393d25f661 add web assembly link 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 21:12:43 -07:00
Nikolaj Bjorner 97cee7d0a4 fix #1576, hopefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-18 07:30:26 -07:00
Nikolaj Bjorner bf6fd1e682 Merge branch 'master' of https://github.com/z3prover/z3 2018-04-18 07:18:56 -07:00