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

13810 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 4defe9b6ab reorder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-28 16:04:37 -07:00
Nikolaj Bjorner 8dde1bf86d compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-28 16:02:32 -07:00
Nikolaj Bjorner 00d35c2777 initialization order 2020-04-28 15:56:50 -07:00
Nikolaj Bjorner a1928a2438 update expected 2020-04-28 15:55:21 -07:00
Lev Nachmanson 97fe2c8609 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson 35e3df49e2 cosmitic changes in int_branch.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson d5162d92ad add an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson aa0f5db511 fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson f8037ffda4 always call find_feasible_solution in move_nbasic_columns_to_bounds() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson ba40a5752f better branching with usage_in_terms() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Lev Nachmanson 3bbf1474f3 na 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-28 15:27:49 -07:00
Nikolaj Bjorner ccce599bad fix #4143 2020-04-28 14:11:39 -07:00
Nikolaj Bjorner fa1197a78f fix #4155 2020-04-28 13:51:25 -07:00
Nikolaj Bjorner 815feddd1a fix #4156 2020-04-28 13:47:26 -07:00
Nikolaj Bjorner fa88dabd10 fix #4135 2020-04-28 13:44:57 -07:00
Nikolaj Bjorner b571e43f85 fix #4146 2020-04-28 13:28:46 -07:00
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