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

473 commits

Author SHA1 Message Date
Nikolaj Bjorner
04ae00048d fix #2567 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 18:48:21 -04:00
Nikolaj Bjorner
69abe1687e backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-14 20:17:07 -04: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
29f0897afc tweaking nlqsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-06 09:42:57 +03:00
Nikolaj Bjorner
68e4ed3c9c fix #2531 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-02 09:59:58 -07:00
Nikolaj Bjorner
000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Nikolaj Bjorner
2e6908bd9e fix #2509, fix issue with model inheritance exposed by #2483 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-27 10:48:22 -03:00
Nikolaj Bjorner
0d9cd7bc2b addressing misc. string bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-24 15:40:15 +01:00
Nikolaj Bjorner
a337a51374 fixes for #2513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Arie Gurfinkel
52acbf1f14 bug in qe_lite 2019-08-09 13:31:49 -07:00
Nikolaj Bjorner
7f073a0585 fix #2452 fix #2451 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-01 16:28:15 +08:00
Nikolaj Bjorner
e1fd167e01 remove stale assertions due to lambda #2446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-30 14:35:09 +08:00
Nikolaj Bjorner
74631265b9 remove stale assertions due to lambda #2446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-30 14:32:06 +08:00
Nikolaj Bjorner
4deb9d2af2 use array interpretations whenever possible for #2378. Also strengthen equality test for lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-14 09:23:29 -04:00
Nikolaj Bjorner
26c1c744aa fix #2396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 17:36:30 -04:00
Nikolaj Bjorner
0bca2aabff remove invocation of debugger 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 17:07:44 -04:00
Nikolaj Bjorner
84990ffa27 fixing #2378 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-12 14:21:22 +01:00
Nikolaj Bjorner
b86432e2a3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:26:50 +07:00
Nikolaj Bjorner
c744b19bce resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
8e2ad4e461 #2379 and #2380 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-04 07:08:47 +07:00
Nikolaj Bjorner
807095a344 fix #2375 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-03 10:04:00 +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
9566d379d6 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 19:44:56 -07:00
Nikolaj Bjorner
3e059a3a3b one must answer the call of the master of compilers #2258 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 05:49:16 +02:00
Nikolaj Bjorner
7399f78dfd disable model compression for regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:40:59 -08:00
Nikolaj Bjorner
ea9e2f6642 fix #2158 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-26 15:13:47 -08:00
Nikolaj Bjorner
c4ee4ffae4 fix pre-prejection> 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-26 07:12:34 -08:00
Nikolaj Bjorner
bef509b02e Yakir! 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 19:20:35 -08:00
Nikolaj Bjorner
d9b4f237fe remove opt dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:18:19 -08:00
Nikolaj Bjorner
46f3b7374c Merge branch 'master' of https://github.com/z3prover/z3 2019-02-25 18:15:28 -08:00
Nikolaj Bjorner
4876426866 project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:15:24 -08:00
Nikolaj Bjorner
4ff940a29e mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-25 18:14:41 -08:00
Nikolaj Bjorner
71e239c08e fix #2061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-06 11:49:47 -08:00
Nikolaj Bjorner
0d400a5ad6 fix bit2bool bug reported by Jianying Li 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-04 07:46:53 -08:00
Nikolaj Bjorner
f8a3300026 introduce proxies to differentiate from arithmetical variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-29 11:13:15 +08:00
Nikolaj Bjorner
e40884725b remove unused euf-mbi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 19:47:48 +08:00
Nikolaj Bjorner
64103038a7 simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 12:20:53 +08:00
Nikolaj Bjorner
0628711c4a simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 12:18:29 +08:00
Nikolaj Bjorner
6a2d54b31e cleanup and doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 11:59:17 +08:00
Nikolaj Bjorner
da95fd7d83 fixing get-arith-vars and extraction of private variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 11:23:52 +08:00
Nikolaj Bjorner
8829fa96de change projection function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 09:38:17 +08:00
Nikolaj Bjorner
076cfa5813 working on revising project0 to project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-26 21:04:35 +08:00
Nuno Lopes
178e5b31e8 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 22:49:06 +00:00
Bruce Mitchener
4bc1b0b8c8 Fix typos. 2018-12-05 21:07:34 +07:00
Nikolaj Bjorner
8248ec879e fix qsat destructor memory allocation #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-28 15:35:46 -08:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner
72400f1869 fix #1927 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-12 03:43:04 -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
Nikolaj Bjorner
6704a4be02
Revert "Made Z3 compile for C++17 with MSVC" 2018-10-15 12:52:19 -07:00