mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 11:17:07 +00:00
Code Activity
16169 commits 23 branches 48 tags 156 MiB
Commit graph

16169 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner 9969809745 #5778 2022-01-21 09:40:06 +01:00
Nikolaj Bjorner a1f7676c81 remove assertion - literals could be assigned but propagation incomplete 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:10:41 +01:00
Nikolaj Bjorner 007af9cb8a fix #5784 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:08:03 +01:00
Nikolaj Bjorner 17280846f8 added comments to explain #5781 2022-01-21 01:40:31 +01:00
Nikolaj Bjorner b1ff4bc24a no normalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 19:21:19 +01:00
Nikolaj Bjorner 75a81af426 fix #5786 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 19:18:23 +01:00
Nikolaj Bjorner af9ae35984 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:43:16 +01:00
Nikolaj Bjorner c527fda0b6 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:41:27 +01:00
Nikolaj Bjorner f1a302bba7 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:38:34 +01:00
Nikolaj Bjorner 7a8c969033 ensure b_internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 13:27:23 +01:00
Nikolaj Bjorner a3d4e9a4e8 adding created to sat/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 11:48:27 +01:00