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 |
|
Murphy Berzish
|
1a5d663138
|
z3str3: disallow leading zeroes in int-to-string conversion
|
2020-04-25 13:25:30 -05:00 |
|
Murphy Berzish
|
d21911c073
|
z3str3: fix support for re.complement and re.intersection
|
2020-04-24 17:49:26 -05: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 |
|
Nikolaj Bjorner
|
9c3f0190f4
|
fix #4069
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-23 20:53:13 -07:00 |
|
Lev Nachmanson
|
8c5993d9a6
|
max term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-23 18:40:16 -07:00 |
|
Lev Nachmanson
|
8921ed56b5
|
fix a bug in Horner heuristic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-23 15:58:53 -07:00 |
|
Nikolaj Bjorner
|
8f297666fe
|
fix #4073
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-23 11:40:24 -07:00 |
|
Anton Kochkov
|
50d58114cf
|
Fix the Julia bindings paragraph in README (#4068)
|
2020-04-23 10:05:50 -07:00 |
|
trinhmt
|
08290230db
|
add docs (#4072)
|
2020-04-23 10:04:10 -07:00 |
|
Nikolaj Bjorner
|
8fe3caa101
|
throttle digit constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 17:55:18 -07:00 |
|
Nikolaj Bjorner
|
c7878e384c
|
fix #4060
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 17:46:16 -07:00 |
|
Nikolaj Bjorner
|
886f4cbee0
|
fix #4029 - propagate digit literals on all units if they haven't already been propagated
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 14:57:43 -07:00 |
|
Nikolaj Bjorner
|
f94abf6512
|
fix #3978
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 13:55:10 -07:00 |
|
Nikolaj Bjorner
|
caa5b09046
|
fix #4050 - have to delay model compression because it may use internal symbols that have to be transformed. model compression is used prior to displaying certificate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 13:33:36 -07:00 |
|