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

16065 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
d6ce05009b try separate x86 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-08 10:14:28 -08:00
Nikolaj Bjorner
6013d5da47 #5755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 14:05:06 -08:00
Nikolaj Bjorner
0bc8518cb5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:53:27 -08:00
Nikolaj Bjorner
199daead50 remove Z3_bool_opt #5757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:52:10 -08:00
Nikolaj Bjorner
7baa4f88b0 build failure 2022-01-06 15:17:57 -08:00
Nikolaj Bjorner
2be71cfc43 #5753 2022-01-06 15:17:37 -08:00
Nikolaj Bjorner
6a3fe514f0 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 14:07:54 -08:00
Nikolaj Bjorner
592b1d7f65 #5752 2022-01-06 13:32:50 -08:00
Nikolaj Bjorner
d14f00d61a with no last model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 13:02:13 -08:00
Nikolaj Bjorner
dadda86bdc #5751 2022-01-06 11:43:17 -08:00
Nikolaj Bjorner
130a0c4aa0 resurrect infinitesimals from maximization function #5720 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-06 08:34:45 -08:00
Nikolaj Bjorner
d7c7fbb8f1 setting roots breaks relevancy propagation 2022-01-05 21:16:25 -08:00
Nikolaj Bjorner
bd8de964f7 more fixes on relevancy 2022-01-04 22:02:28 -08:00
Nikolaj Bjorner
5ec7a66a45 change class name, add comment 2022-01-04 22:02:14 -08:00
Nikolaj Bjorner
964a5cd761 lump java together 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:48:05 -08:00
Nikolaj Bjorner
e943bee625 apply delcypher's todo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:25:14 -08:00
Nikolaj Bjorner
ef3dd32364 some cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-04 20:21:53 -08:00
Nikolaj Bjorner
d1fb831030 relevancy overhaul 2022-01-04 16:03:31 -08:00
Nikolaj Bjorner
4a1975053f cleanup 2022-01-03 17:37:04 -08:00
Nikolaj Bjorner
614c66f1e2 missing relevancy propagation 2022-01-03 17:21:37 -08:00
Nikolaj Bjorner
fc741cf018 rename module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:23:22 -08:00
Nikolaj Bjorner
a086f6218b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:15:41 -08:00
Nikolaj Bjorner
a2a5924e5c purge more 2022-01-03 14:14:09 -08:00
Nikolaj Bjorner
8e3185ffe3 remove dual solver approach 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-03 14:08:01 -08:00
Nikolaj Bjorner
1f964eea90 na 2022-01-03 11:12:28 -08:00
Nikolaj Bjorner
2944449884 #5641 2022-01-03 11:12:09 -08:00
Nikolaj Bjorner
cf08cdff9c #5747 2022-01-03 08:54:54 -08:00
Nikolaj Bjorner
da154b2f7e disable macos with ocaml as it fails too often 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:44:20 -08:00
Nikolaj Bjorner
a71aa113e0 #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:36:17 -08:00
Nikolaj Bjorner
9cbec3b0ca #5641 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-02 19:15:23 -08:00
Nikolaj Bjorner
43e449a805 #5641 2022-01-02 17:53:26 -08:00
Nikolaj Bjorner
d0fb3cba15 #5641 - projection that skips interpreted functions can violate model evaluation. 2022-01-02 17:45:43 -08:00
Nikolaj Bjorner
0ca5e7207e #5746 2022-01-02 11:35:55 -08:00
Nikolaj Bjorner
e84ddb0d9a more #5746 2022-01-02 11:33:21 -08:00
Nikolaj Bjorner
88707f37e7 Better error reporting #5746 2022-01-02 11:31:50 -08:00
Nikolaj Bjorner
543c16c73e Trace unexpected exceptions in or-else code #5746 2022-01-02 10:22:51 -08:00
Nikolaj Bjorner
5cd1fe31fd propagate parent default not add parent default) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-01 20:37:26 -08:00
Nikolaj Bjorner
8245935d41 #5641 add handlers for basic set operations to euf=true 2022-01-01 20:33:17 -08:00
Nikolaj Bjorner
9d3c8a6a2f na 2022-01-01 17:59:31 -08:00
Nikolaj Bjorner
42219204ed sketch replace_all 2022-01-01 17:39:37 -08:00
Nikolaj Bjorner
5672f5cc34 fix #5733 2022-01-01 16:40:48 -08:00
Nikolaj Bjorner
84f514a4f4 throttle ackerman on arrays 2022-01-01 15:33:33 -08:00
Nikolaj Bjorner
a20b577b2f na 2022-01-01 11:26:38 -08:00
Nikolaj Bjorner
ca18150c23 bypass append when src is empty 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-31 16:43:07 -08:00
Nikolaj Bjorner
a44a46a514 fix #5745 2021-12-31 16:41:51 -08:00
Nikolaj Bjorner
9550321064 missed push lambdas 2021-12-31 16:33:06 -08:00
Nikolaj Bjorner
0ef0ed3b94 redoing arrays 2021-12-31 15:51:52 -08:00
Nikolaj Bjorner
aa901c4e88 axiom solver improvements 2021-12-31 11:53:40 -08:00
Nikolaj Bjorner
79f0ceac4c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-30 19:13:23 -08:00
Nikolaj Bjorner
fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00