Nikolaj Bjorner
|
e016979ff6
|
ull
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 18:07:18 -08:00 |
|
Nikolaj Bjorner
|
2882a6708e
|
fix #2957 - arrays are treated as values
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 16:35:13 -08:00 |
|
Nikolaj Bjorner
|
c428db0bf2
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 14:51:58 -08:00 |
|
Nikolaj Bjorner
|
559c3ca012
|
fix #3035
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 10:46:25 -10:00 |
|
Nikolaj Bjorner
|
98bd437e46
|
fix #3039
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 12:45:16 -08:00 |
|
Nikolaj Bjorner
|
3210dce63c
|
fix #3038
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-18 12:38:25 -08:00 |
|
Murphy Berzish
|
698e2ffb0b
|
z3str3: small refactoring to previous commit
|
2020-02-18 08:57:06 -10:00 |
|
Murphy Berzish
|
b4acd44d5e
|
z3str3: fix crash in model construction when a variable has an impossible length assignment
|
2020-02-18 08:57:06 -10:00 |
|
Murphy Berzish
|
da8182419b
|
z3str3: fix indexof out-of-bounds axiom terms
|
2020-02-18 08:57:06 -10:00 |
|
Nikolaj Bjorner
|
f810f25d8d
|
fix #3004
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 19:37:47 -10:00 |
|
Nikolaj Bjorner
|
1959b7c48a
|
fix #3033
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 19:14:46 -10:00 |
|
Nikolaj Bjorner
|
23a474655b
|
fix #3034
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 19:09:46 -10:00 |
|
Nikolaj Bjorner
|
41ab578593
|
remove assert, remove brittle pydoc example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 00:35:47 -10:00 |
|
Nikolaj Bjorner
|
b6ee0b151a
|
fix #3027
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 00:22:48 -10:00 |
|
Nikolaj Bjorner
|
234b53b831
|
fix #3028
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-17 00:20:01 -10:00 |
|
Nikolaj Bjorner
|
8428970a1f
|
fix #3006
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-16 23:46:58 -10:00 |
|
Nikolaj Bjorner
|
d25db0d3e9
|
fix #3026
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-16 15:48:46 -10:00 |
|
Nikolaj Bjorner
|
ccbc4a4943
|
fix #3021
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-16 08:42:05 -10:00 |
|
Nikolaj Bjorner
|
8c35b2092d
|
fix #3022
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-16 08:14:51 -10:00 |
|
Nikolaj Bjorner
|
19ba2948d1
|
fi #3023
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 22:00:36 -10:00 |
|
Nikolaj Bjorner
|
e9c4c23334
|
fix #3017
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:42:22 -10:00 |
|
Nikolaj Bjorner
|
1da64bfe4c
|
fix #3019
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:40:52 -10:00 |
|
Nikolaj Bjorner
|
839d6fd5be
|
fix #3018
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:37:56 -10:00 |
|
Nikolaj Bjorner
|
1d3e9fb76c
|
fix #3009
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:30:09 -10:00 |
|
Nikolaj Bjorner
|
c2f6f2e715
|
fix #3010
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:27:58 -10:00 |
|
Nikolaj Bjorner
|
eb205a5a40
|
fix #3011
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:26:02 -10:00 |
|
Nikolaj Bjorner
|
73662ad60d
|
fix #3016
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:18:15 -10:00 |
|
Nikolaj Bjorner
|
fcc40310c7
|
fix #3015
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:16:34 -10:00 |
|
Nikolaj Bjorner
|
737cf63132
|
fix #3014 by removing unused file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-15 21:13:46 -10:00 |
|
Rose Kunkel
|
aaf2c3bdcc
|
Fix https://github.com/Z3Prover/z3/issues/2998
|
2020-02-14 18:03:59 -10:00 |
|
Nikolaj Bjorner
|
120ca31fae
|
regex pattern per #2986
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-14 17:51:31 -10:00 |
|
Nikolaj Bjorner
|
b71595f5b1
|
fix #3003
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-14 17:51:31 -10:00 |
|
Lev Nachmanson
|
b5276e93bb
|
bug fix in shift_var
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-02-14 16:59:31 -08:00 |
|
Nikolaj Bjorner
|
99b71a9f9e
|
fix #2975, parameter validation to avoid cases where domain of sort is not fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-13 20:20:08 -08:00 |
|
Nikolaj Bjorner
|
b96e203aea
|
fix #2989
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-13 20:20:08 -08:00 |
|
Nikolaj Bjorner
|
8ad939a10f
|
fix #2990
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-13 20:20:08 -08:00 |
|
Nikolaj Bjorner
|
1ce0d7512a
|
fix #2974 by using same code path as qe. It now diverges, but this is due to the use of an uninterpreted predicate which the use of mbp doesn't handle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-13 20:20:08 -08:00 |
|
Murphy Berzish
|
85fd139c7f
|
z3str3: assert precondition for regex linearity axiom
|
2020-02-13 18:19:24 -08:00 |
|
Murphy Berzish
|
0146259ea4
|
z3str3: fix control flow and return paths in regex model construction
|
2020-02-12 12:03:34 -08:00 |
|
Nikolaj Bjorner
|
f5a307073a
|
fixing lut related pass
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-12 11:49:07 -08:00 |
|
Alexey Vishnyakov
|
fdc27d61e4
|
Down compatibility for C++03
|
2020-02-12 10:36:36 -08:00 |
|
Nikolaj Bjorner
|
bbce6bfa07
|
fix #2980
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 22:43:00 -08:00 |
|
Nikolaj Bjorner
|
4f6e3cfe71
|
fix #2976
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 22:20:20 -08:00 |
|
Nikolaj Bjorner
|
17984af4cc
|
disable automatic coersion to reals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 22:06:04 -08:00 |
|
Nikolaj Bjorner
|
4f33c123c9
|
add placeholder
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 20:31:05 -08:00 |
|
Nikolaj Bjorner
|
d02d90dab2
|
add assert to catch bad lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 20:00:48 -08:00 |
|
Nikolaj Bjorner
|
ba2f587c26
|
rm eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 18:39:32 -08:00 |
|
Nikolaj Bjorner
|
c46e36ce58
|
bug fixes to LUT extraction, bug fix for real value case of freedom intervals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 14:25:25 -08:00 |
|
Nikolaj Bjorner
|
806ee85759
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-02-11 14:25:25 -08:00 |
|
Murphy Berzish
|
8d3ed19981
|
z3str3: loop and trace cleanup
|
2020-02-11 12:37:42 -08:00 |
|