Nikolaj Bjorner
|
28a6da4532
|
fix #4902
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-12-18 14:43:00 -08:00 |
|
Nikolaj Bjorner
|
0ef8ebe89f
|
fix #4895
|
2020-12-14 15:05:51 -08:00 |
|
Nikolaj Bjorner
|
9b9d906702
|
fix #4871
|
2020-12-07 22:07:30 -08:00 |
|
Nikolaj Bjorner
|
3c9ada54b6
|
tune hoist-rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 11:25:18 -08:00 |
|
Nikolaj Bjorner
|
768e2c1d0d
|
tune hoist-rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 11:25:17 -08:00 |
|
Nikolaj Bjorner
|
d0e20e44ff
|
booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-07-04 15:56:30 -07:00 |
|
Nikolaj Bjorner
|
278e004385
|
fix #4428, and then there were none, almost
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-04 01:28:26 -07:00 |
|
Nikolaj Bjorner
|
f645ef7677
|
fix #4461
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-06-02 18:08:42 -07:00 |
|
Nikolaj Bjorner
|
2a93ac3d81
|
fix #4200
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-03 18:10:26 -07:00 |
|
Nikolaj Bjorner
|
dc9221e4bd
|
limit iterations on equality solver based on experimenting with #4178
|
2020-05-02 17:10:18 -07:00 |
|
Nikolaj Bjorner
|
dcb75c4b31
|
fix #4174
|
2020-05-01 13:15:51 -07:00 |
|
Nikolaj Bjorner
|
3fc001baea
|
simplifications noticed by trying #4147
The change masks possible bugs in smt.threads and arrays.
|
2020-04-29 12:07:01 -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
|
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
|
44957894ea
|
more checks for #4013
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:43:06 -07:00 |
|
Nikolaj Bjorner
|
339a2568b2
|
fix #4021
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:18:18 -07:00 |
|
Nikolaj Bjorner
|
357ec2fd01
|
fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 13:29:45 -07:00 |
|
Nikolaj Bjorner
|
d0f94055e7
|
fix #3966
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-15 11:05:02 -07:00 |
|
Nikolaj Bjorner
|
5f81913292
|
fix #3951
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 10:51:16 -07:00 |
|
Nikolaj Bjorner
|
299a6f4aee
|
fix #3939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:00:21 -07:00 |
|
Nuno Lopes
|
3313590b95
|
fix #3713: too much caching in dom-simplify for OR expressions
|
2020-04-06 12:11:26 +01:00 |
|
Nikolaj Bjorner
|
426e4cc75c
|
fix #3557
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-03 16:37:59 -07:00 |
|
Nikolaj Bjorner
|
896a1b2048
|
fix #3679
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-02 15:04:56 -07:00 |
|
Nikolaj Bjorner
|
c6b4641050
|
fix #3649
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-01 10:56:27 -07:00 |
|
Nikolaj Bjorner
|
ae447cfdad
|
fix #3603 - false positive, it is an irrational algebraic numeral
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-31 15:15:39 -07:00 |
|
Nikolaj Bjorner
|
a1f68a619d
|
fix #3612
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-31 15:09:12 -07:00 |
|
Nuno Lopes
|
79eb6a0e66
|
reduce_invertible: fix mk_diagonal for BV 0
switch from -x to ~x
|
2020-03-31 12:22:43 +01:00 |
|
Nuno Lopes
|
91497f923a
|
reduce_invertible: recognize (* x -1) as the same as (- x)
|
2020-03-31 10:54:03 +01:00 |
|
Nikolaj Bjorner
|
296e56c28f
|
fix #3575
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 17:26:43 -07:00 |
|
Nikolaj Bjorner
|
330b3cc8d6
|
fix #3584
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 16:50:53 -07:00 |
|
Nikolaj Bjorner
|
b9dd18483c
|
fix #3571
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-30 14:11:36 -07:00 |
|
Nikolaj Bjorner
|
f8dcaa8885
|
'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-27 10:23:00 -07:00 |
|
Nikolaj Bjorner
|
c165f69248
|
fix #3525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-26 09:44:00 -07:00 |
|
Nikolaj Bjorner
|
7996472923
|
fix ? #3370
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-17 10:38:26 -07:00 |
|
Nikolaj Bjorner
|
f06deca7e0
|
fix #3347
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-16 20:21:04 -07:00 |
|
Nikolaj Bjorner
|
c613ab0ba0
|
fix #3286
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-14 11:42:26 -07:00 |
|
Nikolaj Bjorner
|
51e459d02b
|
fix #3294
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-14 10:46:03 -07:00 |
|
Nikolaj Bjorner
|
d530d1314b
|
fix #3276
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-13 11:20:12 -07:00 |
|
Nikolaj Bjorner
|
7bcd3452b8
|
reduce invertible update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-10 21:02:54 -07:00 |
|
Nikolaj Bjorner
|
13883de389
|
fix #3177
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-10 20:13:25 -07:00 |
|
Nikolaj Bjorner
|
99784a92ef
|
fix #3225
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-10 15:10:18 -07:00 |
|
Nikolaj Bjorner
|
89b5b3e69f
|
fix #3223
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-10 13:15:02 -07:00 |
|
Nikolaj Bjorner
|
c7a6721bf1
|
lessen depth expansin in nnf, add cancelation, add ast_marking to avoid repeated sub-expressions #3065
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-09 19:50:43 +01:00 |
|
Nikolaj Bjorner
|
8beb6618d3
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-09 17:51:33 +01:00 |
|
Nikolaj Bjorner
|
be65e9a241
|
fix #3218
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-09 17:37:38 +01:00 |
|
Nikolaj Bjorner
|
c765869d38
|
fix #3176
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-07 12:34:07 +01:00 |
|
Nikolaj Bjorner
|
8b720a0d66
|
fix #3115 fix #3116 regressions from #3111 etc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-02 16:38:33 -08:00 |
|
Nikolaj Bjorner
|
a319f4bf58
|
fix #3104
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-03-02 05:16:48 -08:00 |
|
Nikolaj Bjorner
|
e1ece7e968
|
CTRACE
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-24 20:24:42 -08:00 |
|
Nikolaj Bjorner
|
238ff78374
|
fix #3082
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-24 09:01:31 -08:00 |
|