3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Commit graph

13642 commits

Author SHA1 Message Date
Nikolaj Bjorner c5550e4385 build 2020-04-28 13:18:16 -07:00
Nikolaj Bjorner 1dc8b597b4 fix #4154 2020-04-28 13:17:00 -07:00
Nikolaj Bjorner 1f9e022168 fix #4131 2020-04-28 13:07:25 -07:00
Nikolaj Bjorner e3f712b3cf build 2020-04-28 13:00:56 -07:00
Nikolaj Bjorner 19409a25a6 value sweep 2020-04-27 18:58:43 -07:00
Nikolaj Bjorner 38e0968845 fix #4128 2020-04-27 17:10:48 -07:00
Nikolaj Bjorner 4f462925a0 fix #4116
delta has to be computed based on Simplex tableau not on difference graph.
2020-04-27 17:07:12 -07:00
Nikolaj Bjorner 3a63c3751e fix #4127 2020-04-27 13:27:00 -07:00
Nikolaj Bjorner 8996e8129e fix #4120 2020-04-27 12:06:33 -07:00
Nikolaj Bjorner 4938ea7be6 fix #4123
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-27 11:44:25 -07:00
Nikolaj Bjorner 1c2aa1076b fix #4125 2020-04-27 11:31:02 -07:00
Nikolaj Bjorner a0de244487 pleay nice with alignment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 23:29:42 -07:00
Nikolaj Bjorner d818233063 unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 23:21:48 -07:00
Nikolaj Bjorner 5434f3e31d fix #4105
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 22:59:19 -07:00
Nikolaj Bjorner f1193986c9 fix #4102
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:24:54 -07:00
Nikolaj Bjorner decd69ac73 move to util
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:22:14 -07:00
Nikolaj Bjorner 6d4bd37e15 fix #4104
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Nikolaj Bjorner fc1321f8b3 fix #4104
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Nikolaj Bjorner d37ebb8309 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Nikolaj Bjorner f7a7b9e1f4 fix #4108
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Nikolaj Bjorner 735888145e fix #4112
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Nikolaj Bjorner c2e0491456 fix #4113
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-26 21:04:28 -07:00
Lev Nachmanson 0499b6b64a some fixes in branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-26 20:35:22 -07:00
Nikolaj Bjorner 029edcfabd fix #4114 2020-04-26 16:17:42 -07:00
Nikolaj Bjorner 51c3778354 fix #4106 2020-04-26 16:17:42 -07:00
Lev Nachmanson 530f77281c fixes in branching
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-04-26 16:13:47 -07:00
Nikolaj Bjorner 236edad8dc fix #4111 2020-04-26 14:44:50 -07:00
Nikolaj Bjorner dc852a6f83 fix #4110 2020-04-26 14:13:58 -07:00
Nikolaj Bjorner d3094291d3 fix #4107 2020-04-26 13:45:29 -07:00
Nikolaj Bjorner 16d34b9fcc fix #4100 2020-04-26 13:30:13 -07:00
Nikolaj Bjorner 626d0186c8 fix #4098 2020-04-26 13:17:40 -07:00
Nikolaj Bjorner f9193809ea add recfun rewriting, remove quantifier based recfun 2020-04-26 12:59:51 -07:00
Nikolaj Bjorner 7f1b147cba remove 2020-04-25 15:52:02 -07:00
Nikolaj Bjorner 9f378bb1b9 #4099 2020-04-25 15:51:18 -07:00
Nikolaj Bjorner a884201d62 remove using insert_if_not_there2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-25 15:08:51 -07:00
Nikolaj Bjorner 9ea1cf3c5c na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-25 13:13:25 -07:00
Nikolaj Bjorner 785c9a18ca fix #4049
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 11:58:48 -07:00
Nikolaj Bjorner 6ab83466d9 fix #4082
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 11:33:19 -07:00
Nikolaj Bjorner a3844af94b fix #4081
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 10:44:20 -07:00
Nikolaj Bjorner c3b33aae8a fix #4090 fix #4088 fix #4085
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 10:37:43 -07:00
Nikolaj Bjorner 470e87afe9 update rewite modality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 01:12:06 -07:00
Nikolaj Bjorner 851c38f64a fix #4086
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 00:52:02 -07:00
Nikolaj Bjorner 2793c3af2c more replace rewrites #4084
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 00:48:02 -07:00
Nikolaj Bjorner 03ba268219 more replace rewrites #4084
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-24 00:25:36 -07:00
Nikolaj Bjorner 7597396dd0 fix #4080
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 22:58:20 -07:00
Nikolaj Bjorner 6ff61d1f80 fix #4062
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 22:43:14 -07:00
Nikolaj Bjorner eb2d7d3e81 fix #4079
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 22:35:33 -07:00
Nikolaj Bjorner 64cb5cad81 remove spurious output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 22:12:38 -07:00
Nikolaj Bjorner 04fec3f6a0 fix #4076
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 21:34:20 -07:00
Nikolaj Bjorner cc8cd2cc2f na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-04-23 21:28:19 -07:00