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

2084 commits

Author SHA1 Message Date
Nikolaj Bjorner
1287572f4f add complexity throttle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 14:31:31 -08:00
Nikolaj Bjorner
f5164d166b unused / return warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 14:25:18 -08:00
Nikolaj Bjorner
13e335f062 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 14:14:46 -08:00
Nikolaj Bjorner
98bfbc2d62 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:59:45 -08:00
Nikolaj Bjorner
469f618742 build dependencies, invariant annotation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 13:48:27 -08:00
Nikolaj Bjorner
5e0799225d adding pdd-grobner 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-18 12:03:13 -08:00
Nikolaj Bjorner
ca0a52c930 some const qualifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 21:59:05 -08:00
Nikolaj Bjorner
1680585827 swap sub with minus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 21:46:55 -08:00
Nikolaj Bjorner
a744a465e6 pdd fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 21:25:18 -08:00
Nikolaj Bjorner
f2149fb5a6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 17:14:51 -08:00
Nikolaj Bjorner
f7eb5f8840 merge unary minus 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 17:10:35 -08:00
Nikolaj Bjorner
9e4a7ae4b8 add pdd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 16:59:33 -08:00
Nikolaj Bjorner
6fa7e98ff9 cmake 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 10:10:14 -08:00
Nikolaj Bjorner
1fdde9e056 move bdd to separate space 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-17 10:03:01 -08:00
Nikolaj Bjorner
64dd4e1c83 fix #2659 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-25 10:42:21 -07:00
Nikolaj Bjorner
a921b4ff4a fix #2643 - fuzzers are here to get you @lorisdanton 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 18:19:13 -07:00
Nikolaj Bjorner
d0cf1458e3 fix #2630 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 04:12:06 -07:00
Nikolaj Bjorner
7c10fb83a0 fix #2615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 19:00:14 -07:00
Nikolaj Bjorner
39edf73e78 fix #2613 fix #2612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-05 16:57:51 -07:00
Nikolaj Bjorner
c8908e81aa fix #2609 fix #2610 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-02 16:59:35 -07:00
Nikolaj Bjorner
88f0e4a64c fix #2592 #2593 #2597 #2573 - duplicates, also fix #2603 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-01 13:14:12 -07:00
Nikolaj Bjorner
301209cda6 fix #2595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-28 17:44:25 -07:00
Nikolaj Bjorner
98c3887460 fix #2595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-28 17:43:48 -07:00
Nikolaj Bjorner
67c4777514 fix #2548 fix #2530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:04 +02:00
Nikolaj Bjorner
db274ebe01 relax condition for distributing extract over ite #2359 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-23 16:48:42 -07:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Nikolaj Bjorner
1ca3381390 fix #2319 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:42:19 -07:00
Bruce Mitchener
a12de12515 Use const& to reduce copies. 2019-06-02 09:58:32 +07:00
Nikolaj Bjorner
dd452e0ac1 eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 15:29:27 -07:00
Nikolaj Bjorner
f99384c6a3 fix nightly regression from solve-eqs context solver addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 04:17:43 -07:00
Nikolaj Bjorner
28ce701e17 fixing 2267 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-06 15:31:55 +02:00
Nikolaj Bjorner
606754c09a fix #2262 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-30 19:04:02 -07:00
Nikolaj Bjorner
0acc042bf7 fix #2120 fix #2122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 17:15:38 +01:00
Nikolaj Bjorner
9fde9fe3a2 fix #2122 for code that isn't exception safe 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-02 19:49:16 +01:00
Nikolaj Bjorner
b6bf299b8b update upolynmial test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:41:50 -08:00
Nikolaj Bjorner
f4d03edf22 remove unreachable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:54:30 -08:00
Bruce Mitchener
bcfa8045fa Sink some values into loops. 
This removes some dead stores that happen prior to the loop and
ensure that no one is looking at the values outside of the
loop.
 2018-11-30 23:12:21 +07:00
Bruce Mitchener
3149d7f7a4 Fix typos. 2018-11-30 22:19:30 +07:00
Bruce Mitchener
a3281a02db mk_coeffs_without was inadvertently copying src. 
Pass it via ref.
 2018-11-28 20:12:47 +07:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner
88fb826a03 overhaul stoi and itos to fix #1957 and related 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 18:50:20 -08:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Michał Janiszewski
cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Bruce Mitchener
a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner
fc4627a24f force the new arithmetic solver for QF_LIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 16:33:48 -07:00
Nikolaj Bjorner
de454db58c guard expensive ite rewrites under configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 14:17:39 -07:00
Nuno Lopes
009708ed07 remove unneeded creation of tmp mpz_manager 2018-07-09 10:52:27 +01:00
Nikolaj Bjorner
20fc573d5b add laxer check for oeq_quant_intro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-27 11:24:56 -07:00
Nikolaj Bjorner
bf4edef761 fix mbi arithmetic solver for lower bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 06:37:47 -07:00
Nikolaj Bjorner
baa96909cc mb-skolem for arithmetic with model repair 
The contract is that users of mb-skolem ensure that
interface equalities are preserved (by adding a
sufficient set of disequalities, such as a chain
x1 < x2 < x3 .., to force that solutions for
x_i does not clash).

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 17:26:04 -07:00