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 |
|
Nikolaj Bjorner
|
95a78b2450
|
updates to seq and bug fixes (#4056)
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4037
* nicer output for skolem functions
* more overhaul of seq, some bug fixes
* na
* added offset_eq file
* na
* fix #4044
* fix #4040
* fix #4045
* updated ignore
* new rewrites for indexof based on #4036
* add shortcuts
* updated ne solver for seq, fix #4025
* use pair vectors for equalities that are reduced by seq_rewriter
* use erase_and_swap
* remove unit-walk
* na
* add check for #3200
* nits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* name a type
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove fp check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* remove unsound axiom instantiation for non-contains
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix rewrites
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4053
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4052
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-22 13:18:55 -07:00 |
|
Alberto Garcia Illera
|
53c14bd554
|
Use Position Independent Code flag on Static library builds (#4043)
Not compiling libz3 with `-fPIC` may lead to errors when using it in his static flavor from a shared library.
Related https://github.com/Z3Prover/z3/issues/4038
|
2020-04-22 10:52:05 -07:00 |
|
Nuno Lopes
|
5ec04f7fd2
|
forgot to remove unneeded class field
|
2020-04-22 15:30:16 +01:00 |
|
Nuno Lopes
|
220bc7fcd9
|
fix #4048: incorrect bvurem rewrite when divisor=0
also, always enable this rewrite, since it shrinks formula size globally
|
2020-04-22 15:26:30 +01:00 |
|
Nikolaj Bjorner
|
dd064a5554
|
delay digit axioms until solving itos succeeds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-20 00:32:48 -07:00 |
|
Nikolaj Bjorner
|
e3e6959b70
|
fix #4026
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 23:30:37 -07:00 |
|
Nikolaj Bjorner
|
c8b9eba069
|
fix #4028
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 23:10:00 -07:00 |
|
Nikolaj Bjorner
|
ad8eb8fdcb
|
#4024
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 22:44:02 -07:00 |
|
Nikolaj Bjorner
|
e1fa04b365
|
disable breaking change to model generation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 16:53:20 -07:00 |
|
Nikolaj Bjorner
|
eded7d023d
|
fix #4006
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 16:00:03 -07:00 |
|
Nikolaj Bjorner
|
f76c6424f2
|
another memory managment leak fix. Relates to different leak exposed by #3997
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:58:42 -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
|
fcc34a07b2
|
fix #4019
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-19 12:36:34 -07:00 |
|