mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity
14201 commits 24 branches 48 tags 158 MiB
Commit graph

14201 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nuno Lopes
23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner
48a9defb0d fix #1484 'regression' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-09 15:09:25 -07:00
Nikolaj Bjorner
6b380811b8 fix #4524 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-09 15:05:55 -07:00
Nikolaj Bjorner
65e6b73873 fix #4538 - regression when renaming family from special_relations to specrels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 14:46:40 -07:00
Nikolaj Bjorner
80cc45c5c1 display justifications compactly for tracing #4575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 13:32:41 -07:00
Nikolaj Bjorner
ab7b8b6ec5 fix #4572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:58:44 -07:00
Nikolaj Bjorner
061abd153c fixing #4515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
ec3066c28a #4532 - arithmetic using SAT for interpreted atoms such as (< 0 0) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
e1a0a2e536 give up on addition subterms in monomial decomposition caused by disabling rewriter.flat seems to be corner case exercised in #4532. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner
69afd9f6bd formatting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:31 -07:00
Nikolaj Bjorner
9bcda408ba towards closing small domain equality enforcement gap #4515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:31 -07:00
Christoph M. Wintersteiger
3776588375
Clarify bit-blasting of fp.neg. Fixes #4466. 2020-07-08 18:24:08 +00:00
Christoph M. Wintersteiger
c59519bf9c
Add missing FP conversion. Fixes #4470. 2020-07-08 17:56:25 +00:00
Nikolaj Bjorner
688d38d868 typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 19:07:26 -07:00
Nikolaj Bjorner
4e77984c57 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:59:20 -07:00
Nikolaj Bjorner
4b346ef693 enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:58:42 -07:00
Nikolaj Bjorner
4a8533e41f enable binary string access to unsigned numerals over API #4568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-07 18:17:54 -07:00
Nikolaj Bjorner
2d358a9a50 fix #4565 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-06 17:07:37 -07:00
Nuno Lopes
ca97bfb4b8 fix build 2020-07-05 11:44:12 +01:00
Nikolaj Bjorner
006418e027 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 23:34:21 -07:00
Nikolaj Bjorner
f380d4cf83 mpfx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:25:32 -07:00
Nikolaj Bjorner
74eb401c3b addrecdef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 18:18:25 -07:00
Nikolaj Bjorner
51d43c04ea st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:13:04 -07:00
Nikolaj Bjorner
2bb712c9da ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:09:08 -07:00
Nikolaj Bjorner
5ea145ce26 ml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:08:22 -07:00
Nikolaj Bjorner
bf14444f7d st 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 17:07:07 -07:00
Nikolaj Bjorner
f3b51db891 ml build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 16:22:01 -07:00
Nikolaj Bjorner
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
10d0404175 add rec decl/def to ML #4563 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:38:32 -07:00
Lev Nachmanson
62b9630c4b remove unicode from hnf_cutter.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
7a4eed0216 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
49e49d6bb6 add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
80a4da9b1d add comments to hnf_cutter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
fff6a94de4 cheap_eqs - fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
61da368ee3 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
f4502ff952 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
1695379dc9 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
a1c5cff541 cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
29b3f438bc cheap_eqs - work on fixed_phase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
cb3ebac3dd cleanup lp_bound_propagator.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00
Lev Nachmanson
b996bc1f02 remove cheap equalities with the table 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-07-04 09:33:45 -07:00