Nikolaj Bjorner
|
1269776777
|
remove experimental option. Fix #4806
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-20 11:46:19 -08:00 |
|
Nikolaj Bjorner
|
ac1b3fc6f2
|
fix delay blasting and relevancy
|
2020-11-20 11:12:55 -08:00 |
|
Nikolaj Bjorner
|
9f34af5e18
|
update justifications only at level 0
|
2020-11-20 11:12:55 -08:00 |
|
Nikolaj Bjorner
|
ee04bfd174
|
fix equality propagation
|
2020-11-20 11:12:55 -08:00 |
|
Nikolaj Bjorner
|
a475e7cf5a
|
Add gcd test to bv-rewriter
|
2020-11-20 11:12:54 -08:00 |
|
Nikolaj Bjorner
|
6506d33b35
|
Add GCD test
|
2020-11-20 11:12:54 -08:00 |
|
Nikolaj Bjorner
|
b7b7970c4a
|
guard table erasure for representative
|
2020-11-20 11:12:54 -08:00 |
|
Nuno Lopes
|
40159a3a96
|
fix single-thread build
|
2020-11-19 21:46:32 +00:00 |
|
John Regehr
|
0fa88efc2b
|
scoped_timer: wait for timer thread before main thread continues (#4803)
|
2020-11-19 21:42:55 +00:00 |
|
Nikolaj Bjorner
|
e16acd0965
|
move std::function initializer to beginning of class
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-16 17:02:15 -08:00 |
|
Nikolaj Bjorner
|
f6f594e21d
|
fix missing equality propagation in new bv solver
|
2020-11-16 16:22:56 -08:00 |
|
Nikolaj Bjorner
|
36e40a296f
|
add logging for rewriter.flat
|
2020-11-16 11:20:33 -08:00 |
|
Nikolaj Bjorner
|
85a20791db
|
fix relevancy tracking in new solver
|
2020-11-16 11:20:17 -08:00 |
|
Nikolaj Bjorner
|
36e9412252
|
fix #4796
|
2020-11-16 11:19:54 -08:00 |
|
Nikolaj Bjorner
|
98db260a93
|
relax unhandled condition
|
2020-11-14 14:58:43 -08:00 |
|
Nikolaj Bjorner
|
49a0266c6a
|
na
|
2020-11-13 17:05:56 -08:00 |
|
Nikolaj Bjorner
|
9fa17a432a
|
bug fixes in nullability check
@veanes @cdstanford
|
2020-11-13 17:05:10 -08:00 |
|
Nikolaj Bjorner
|
c15001bf69
|
#4532
https://github.com/Z3Prover/z3/issues/4532#issuecomment-726867868
|
2020-11-13 11:45:59 -08:00 |
|
Nikolaj Bjorner
|
71ac40ca23
|
fix #4793
|
2020-11-13 11:45:05 -08:00 |
|
Nikolaj Bjorner
|
cb4e5197fa
|
#4740
Fix https://github.com/Z3Prover/z3/issues/4740#issuecomment-712092917
|
2020-11-12 16:55:07 -08:00 |
|
Nikolaj Bjorner
|
7f869e513b
|
fix #4792
|
2020-11-12 13:23:34 -08:00 |
|
Nikolaj Bjorner
|
d61f30fdc6
|
force flat for solver 2, fix #4789
|
2020-11-12 13:01:38 -08:00 |
|
Nikolaj Bjorner
|
5d10cb7af4
|
fix #4791 - diff is left associative
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-11 18:07:05 -08:00 |
|
Nikolaj Bjorner
|
72e57f550d
|
update release similar to nightly
|
2020-11-11 17:38:07 -08:00 |
|
Nikolaj Bjorner
|
7e68d546ba
|
na
|
2020-11-11 17:37:07 -08:00 |
|
Nikolaj Bjorner
|
aced115b70
|
model validation
|
2020-11-11 17:37:07 -08:00 |
|
Nikolaj Bjorner
|
16db8bf49e
|
add model validation
|
2020-11-11 17:37:07 -08:00 |
|
Nikolaj Bjorner
|
b5aab7ec2a
|
fix clone
|
2020-11-11 17:37:06 -08:00 |
|
Nikolaj Bjorner
|
9704733693
|
fix #4790
|
2020-11-11 17:37:06 -08:00 |
|
Nikolaj Bjorner
|
fdd3e6c4c2
|
Update nightly.yaml for Azure Pipelines
|
2020-11-10 16:26:06 -08:00 |
|
Nikolaj Bjorner
|
8c60e7b8f4
|
Update nightly.yaml for Azure Pipelines
|
2020-11-10 16:24:56 -08:00 |
|
Nikolaj Bjorner
|
41cc037204
|
change manylinux to ubuntu-latest
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-10 16:17:35 -08:00 |
|
Lev Nachmanson
|
4810b4cac2
|
add a comment in nla_order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-11-10 11:12:28 -08:00 |
|
Lev Nachmanson
|
fc5e5a2098
|
add a comment in nla_order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-11-10 11:11:42 -08:00 |
|
Nikolaj Bjorner
|
fdedeed7ae
|
additional sign related fix for #4740 https://github.com/Z3Prover/z3/issues/4740#issuecomment-721508240
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-10 10:50:13 -08:00 |
|
Nikolaj Bjorner
|
5ace60c812
|
enforce guard option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-10 09:22:32 -08:00 |
|
Nikolaj Bjorner
|
672e392386
|
guard
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-10 08:01:29 -08:00 |
|
Nikolaj Bjorner
|
be50f38903
|
enforce sign coherence #4740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 14:30:00 -08:00 |
|
Nikolaj Bjorner
|
638ef9ed03
|
enforce sign coherence #4740
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 14:28:49 -08:00 |
|
Nikolaj Bjorner
|
e955bd09e5
|
push equality for #4740
https://github.com/Z3Prover/z3/issues/4740#issuecomment-711460353
|
2020-11-09 13:08:46 -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
|
4d26aabd83
|
fix bug in rewriting of power
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-09 07:12:37 -08:00 |
|
Nikolaj Bjorner
|
f78980c81c
|
fix rewriting of power
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-08 20:58:16 -08:00 |
|
Johannes Kanig
|
7d205f1cf0
|
TB08-009 fix z3 build on windows (#4782)
It seems that VS 15.0 doesn't like this usage of "enum"
Change-Id: Ie7eba81ad9fd990aa436d323dc848d1b0f2c4370
|
2020-11-08 20:47:25 -08:00 |
|
Nikolaj Bjorner
|
864eaf8bf8
|
remove unsound rewrite #4778
|
2020-11-08 17:48:51 -08:00 |
|
Nikolaj Bjorner
|
e2c1436cc8
|
fix #4775
|
2020-11-08 17:18:18 -08:00 |
|
Nikolaj Bjorner
|
89ffb45c4f
|
fixes to bv/dual-solver,
|
2020-11-08 17:18:18 -08:00 |
|
Nikolaj Bjorner
|
a4354c960c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-08 17:18:17 -08:00 |
|
Nikolaj Bjorner
|
752f08c9d6
|
check_feasible is called after column is added for fixed variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-11-08 17:18:17 -08:00 |
|