mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
16180 commits 49 branches 53 tags 182 MiB
Commit graph

16180 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6202cd5394 fix #5842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 17:38:19 +02:00
Nikolaj Bjorner
aa6ec418e3 move idiv test to after cuts/branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-14 19:50:49 +02:00
Nikolaj Bjorner
9a4d6cee6c overhead with push-ite on shared terms 2022-02-14 19:36:14 +02:00
Nikolaj Bjorner
3d26b501e7 fix #5827 #5828 2022-02-14 10:31:04 +02:00
Nikolaj Bjorner
d745d03afd switch to vs 2022 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-10 08:55:43 +02:00
Nikolaj Bjorner
81e94b2154 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-09 12:10:01 +02:00
Nikolaj Bjorner
07d02ea415 fix #5829 2022-02-09 12:08:36 +02:00
Nikolaj Bjorner
4f6fcf8ea7 fix #5814 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-08 10:20:19 +02:00
Nikolaj Bjorner
0059e88036 fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 20:10:32 +02:00
Nikolaj Bjorner
9958cab5cc fix #5808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-07 07:43:30 +02:00
Nikolaj Bjorner
3f3d058567 extract also units from search state 2022-02-07 06:16:22 +02:00
Kaleb Crans
d4ea67a6e7
Fix a few typos in README (#5782) 2022-02-06 19:47:47 +02:00
Nikolaj Bjorner
03ff3201b9 block recursive definitions with lambdas until they are properly supported #5813 2022-02-06 08:57:58 +02:00
Nikolaj Bjorner
1c10ce4070 #5815 - surface multi-arity arrays over python API 2022-02-06 08:40:56 +02:00
Nikolaj Bjorner
8a84cacfea add tuple support for __getitem__ #5815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-06 04:02:12 +02:00
Nikolaj Bjorner
e9dad84b85 update documentation comments 2022-02-06 03:35:32 +02:00
Nikolaj Bjorner
9d655cc658 track all unhandled operators instead of latest 2022-02-04 22:07:29 -08:00
Nikolaj Bjorner
474949542e Merge branch 'master' of https://github.com/z3prover/z3 2022-02-04 13:08:59 -08:00
Nikolaj Bjorner
05e28e4344 fix #5812 2022-02-04 13:08:52 -08:00
Nikolaj Bjorner
6a412f7f04 allow to pass Booleans as arguments to arithmetic expressions 2022-01-31 12:00:54 -08:00
Nikolaj Bjorner
994c7ef52d format 2022-01-31 12:00:26 -08:00
Nikolaj Bjorner
1e0d49512b call mux finder 2022-01-31 12:00:16 -08:00
Nikolaj Bjorner
4392b88718 return negated literal when expression is "not" 2022-01-31 12:00:00 -08:00
Nikolaj Bjorner
7ddfc54250 shortcut negation 2022-01-31 11:58:02 -08:00
Nikolaj Bjorner
f3fc6a50f3 formatting 2022-01-31 11:57:42 -08:00
Nikolaj Bjorner
6422b783b2 fix mux extraction to check for top-level assertion 2022-01-31 11:57:16 -08:00
Nikolaj Bjorner
62bb234251 expose extract roots as separate 2022-01-31 11:56:44 -08:00
Nikolaj Bjorner
a326ad4cd9 flag incomplete on lambdas #5803 2022-01-31 11:54:06 -08:00
Nikolaj Bjorner
a189ca8b60 truncation directive #5805 2022-01-31 10:50:46 -08:00
Nikolaj Bjorner
773e829c58 #5804 2022-01-31 10:16:09 -08:00
Nikolaj Bjorner
913b90f7aa fix #5802 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-30 10:42:34 -08:00
Nikolaj Bjorner
2551631957 mul overflow #5797 2022-01-29 09:15:38 -08:00
Nikolaj Bjorner
5e81c1220c #5797 probably still wrong wrt underflow. 2022-01-27 12:48:15 -08:00
Nikolaj Bjorner
9e5b6e0c9c #5778 2022-01-27 12:12:58 -08:00
Nikolaj Bjorner
4da930b490 #5794 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:50:48 -08:00
Nikolaj Bjorner
a621041308 fix #5795 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:45:38 -08:00
Nikolaj Bjorner
461e71017d fix #5792 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 15:54:44 -08:00
Nikolaj Bjorner
53f72d9cbe updated mini 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 15:44:49 -08:00
Nikolaj Bjorner
c6539deb61 fixing null check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 17:25:42 +01:00
Nikolaj Bjorner
435f79eab0 tup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:40:55 +01:00
Nikolaj Bjorner
9294b2ceb2 created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:33:23 +01:00
Nikolaj Bjorner
3de9d37772 fix overrides for created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 16:24:08 +01:00
Nikolaj Bjorner
bf6454dccc throw error if created-eh has not been registered 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 13:01:57 +01:00
Nikolaj Bjorner
ea6827505e add missing callback to m_created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 10:13:09 +01:00
Nikolaj Bjorner
f639a7e1bc add marker for top-level expression in rule. 2022-01-24 15:20:44 +01:00
Nikolaj Bjorner
61ab72b6a3 fix #4869 2022-01-24 15:14:47 +01:00
Nikolaj Bjorner
3b8c0b7ae6 fix #5791 2022-01-24 15:11:24 +01:00
Nikolaj Bjorner
20f9814939 fix #5789 
fix incorrect constant folding
 2022-01-24 09:42:14 +01:00
Nikolaj Bjorner
d02235fe08 #5778 
not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.
 2022-01-22 16:16:48 +01:00
Hennadii Chernyshchyk
85f6456655
Add missing constness (#5787) 2022-01-21 15:32:25 +01:00