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

14742 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
d591bf62c1 add to readme #4575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-27 09:35:50 -07:00
Nikolaj Bjorner
9624df942f na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-27 09:24:35 -07:00
Nikolaj Bjorner
a08082e392 fix #4594 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-27 09:22:53 -07:00
Nikolaj Bjorner
ae502bc2c4 simplify a few of the several axiom trace commands 2020-07-26 18:02:34 -07:00
Nikolaj Bjorner
c7704ef9af pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 17:52:28 -07:00
Nikolaj Bjorner
ac39ddb43f flush gmc for sat-preprocessor model bug #4532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 14:30:48 -07:00
Nikolaj Bjorner
e8ef9a85a4 fix #4327 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 13:22:13 -07:00
Nikolaj Bjorner
4be6927460 unused variable warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 13:22:12 -07:00
Nikolaj Bjorner
78afa2527c unused variable warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 13:22:12 -07:00
Nikolaj Bjorner
4d586c2c13 remove stale references to gac/csc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 12:03:03 -07:00
Nikolaj Bjorner
105f97d3ee #4582 again 2020-07-25 15:12:25 -07:00
Nikolaj Bjorner
2133ba06a7 prepare for theory variables othe rthan seq/re 2020-07-25 15:11:13 -07:00
Nikolaj Bjorner
f789573d12 prepare for alternative axiom 2020-07-25 15:10:39 -07:00
Nikolaj Bjorner
2d4839f89e #4582 again 2020-07-25 15:09:30 -07:00
Nikolaj Bjorner
1059f6d3b8 #4582 again 2020-07-25 11:54:05 -07:00
Nikolaj Bjorner
963daab268 #4582 again 2020-07-25 11:18:20 -07:00
Nikolaj Bjorner
e63992c8bd fix #4589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-24 15:46:54 -07:00
Nikolaj Bjorner
780346c7ca address model generation bugs raised in #4518 and #4324 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-24 13:22:19 -07:00
Nikolaj Bjorner
e1d2b88a82 access polynomial expressions from algebraic numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-23 15:08:11 -07:00
Nikolaj Bjorner
a6a041ec5d setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-23 13:43:54 -07:00
Nikolaj Bjorner
71a32f5bb2 remove unused 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 11:38:27 -07:00
Nikolaj Bjorner
45855fce06 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 10:45:29 -07:00
Nikolaj Bjorner
dd5e2e8930 check for 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 10:44:00 -07:00
Nikolaj Bjorner
640cf1809d
Merge pull request #4585 from iscottb122/dotnet_fp_significand 
Return significand bits correctly (dotnet API). Fixes #4584
 2020-07-22 09:59:30 -07:00
Iain Scott
b6867d69c2
Return significand bits correctly (dotnet API). Fixes #4584 2020-07-22 16:57:33 +01:00
Nikolaj Bjorner
ed58175e1b issue #4582 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-21 18:23:41 -07:00
Nikolaj Bjorner
aab50ff3f5 fixing bugs reported in #4518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-21 15:50:19 -07:00
Nikolaj Bjorner
b1824fea10 fix lifetimes for crashes in #4525 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-21 12:53:56 -07:00
Nikolaj Bjorner
f17ead21f9 fix #4578 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-21 10:11:39 -07:00
Nikolaj Bjorner
1d8d85add9 fix #4575 - correction set resolution only works with uniform weights 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 15:05:06 -07:00
Nikolaj Bjorner
ebce0b3612 fix #4577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 14:40:45 -07:00
Nikolaj Bjorner
61b85d7123 verbosity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 14:11:59 -07:00
Nikolaj Bjorner
e8b5abe63e revert - copy over xml in mk-dist mode #4578 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 11:17:29 -07:00
Nikolaj Bjorner
a7b71239ae copy over xml in mk-dist mode #4578 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 10:22:57 -07:00
Nikolaj Bjorner
00491148f0 string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 10:22:57 -07:00
Nikolaj Bjorner
549ef0e052 fix typos #4573 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-20 10:22:57 -07:00
Christoph M. Wintersteiger
a298091322
Fix for fp.roundToIntegral of tiny, denormal floats. Fixes #4190. 2020-07-17 15:58:01 +00:00
Christoph M. Wintersteiger
2ef57d7f8d
Fix FP rounding of huge exponents. Fixes #3776. 2020-07-17 13:42:12 +00:00
Christoph M. Wintersteiger
d3ae40130a
Fix rounding bug in mpf_manager. Fixes #2970. 2020-07-16 12:39:12 +00:00
Christoph M. Wintersteiger
ccdae7af24
Fix for corner-case in fp.roundToIntegral. Fixes #2894. 2020-07-16 11:58:18 +00:00
Christoph M. Wintersteiger
c321fb7726
Correctly report unsupported features in bvarray2uf_rewriter. Fixes #4046 and #4047. 2020-07-15 16:16:29 +00:00
Christoph M. Wintersteiger
7dd28708a1
Fix bug in qprofdiff. Fixes #4521. 2020-07-15 15:13:11 +00:00
Nuno Lopes
b7caabbd0f fix crashes with MSVC 2019 2020-07-14 13:14:44 +01:00
Nuno Lopes
aeac0b46a0 remove copy 2020-07-14 12:26:49 +01:00
Nuno Lopes
d1a0e83423 fix crash 2020-07-13 14:25:12 +01:00
Nuno Lopes
122f5a1464 remove unused field 2020-07-12 23:12:00 +01:00
Nuno Lopes
90fc8d854f add rval methods to scoped_vector 2020-07-12 22:16:24 +01:00
Nuno Lopes
f30e8ccec3 fix crashes due to my last commit 2020-07-12 19:53:22 +01:00
Nuno Lopes
bb26f219fe remove unneeded constructors (last round) 2020-07-12 17:41:57 +01:00
Nuno Lopes
44ec259c4c fix python test 2020-07-11 22:33:47 +01:00