Nikolaj Bjorner
|
5e0c34cae2
|
fix #3953
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 09:43:03 -07:00 |
|
Nikolaj Bjorner
|
2a0537af69
|
fix #3954
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 08:17:57 -07:00 |
|
Nikolaj Bjorner
|
b8c069c6b7
|
fix #3955
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 08:13:17 -07:00 |
|
Nikolaj Bjorner
|
f564c325d3
|
fix #3957
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:46:10 -07:00 |
|
Nikolaj Bjorner
|
d7d6877031
|
fix #3958
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:34:03 -07:00 |
|
Nikolaj Bjorner
|
387964f508
|
fix #3960 fix #3959
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-14 06:30:54 -07:00 |
|
Nikolaj Bjorner
|
0f697830fc
|
spelling
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 19:08:05 -07:00 |
|
Nikolaj Bjorner
|
fe7146d93b
|
fix #3913 - change assumption tracking to be granular based on disabled guards
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 19:06:12 -07:00 |
|
Nikolaj Bjorner
|
e1027790ae
|
more to #3926
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 16:04:54 -07:00 |
|
Lev Nachmanson
|
7caae3f5d2
|
small improvements in tableau in rows and bound propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-13 16:04:25 -07:00 |
|
Lev Nachmanson
|
90793931b1
|
small changes in one_iteration_tableau_rows
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-13 16:04:25 -07:00 |
|
Nikolaj Bjorner
|
9223f611ba
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:49:27 -07:00 |
|
Nikolaj Bjorner
|
9f42338de8
|
fix #3926
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:43:27 -07:00 |
|
Nikolaj Bjorner
|
299a6f4aee
|
fix #3939
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 14:00:21 -07:00 |
|
Nikolaj Bjorner
|
d3db2af81d
|
fix #3941
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 13:15:15 -07:00 |
|
Nikolaj Bjorner
|
b4e7730034
|
fix #3938
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 13:05:53 -07:00 |
|
Nikolaj Bjorner
|
6a5695463f
|
fix #3943
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 12:58:18 -07:00 |
|
Nikolaj Bjorner
|
5dafd1fe25
|
fix #3945
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 10:46:47 -07:00 |
|
Nikolaj Bjorner
|
5c4f775b1b
|
fix #3935
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-13 10:00:42 -07:00 |
|
Nikolaj Bjorner
|
01c12c951c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 18:01:54 -07:00 |
|
Nikolaj Bjorner
|
84a4d9850b
|
fix #3936
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 18:01:20 -07:00 |
|
Nikolaj Bjorner
|
75a460cc15
|
fix #3932
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 17:49:50 -07:00 |
|
Nikolaj Bjorner
|
9b609af8fc
|
fix #3924
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 16:19:54 -07:00 |
|
Nikolaj Bjorner
|
51eaf84eed
|
fix #3931
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 15:37:18 -07:00 |
|
Nikolaj Bjorner
|
c85113acdb
|
fix #3928
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-12 15:25:08 -07:00 |
|
Nikolaj Bjorner
|
db9d6d12fc
|
fix #3836 remove unused and buggy hoist_cmul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 15:27:18 -07:00 |
|
Nikolaj Bjorner
|
97af74d8cb
|
fix #3917 remove non-native mode for recfun
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 14:19:26 -07:00 |
|
Nikolaj Bjorner
|
0ee79182d4
|
fix #3911
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 14:09:09 -07:00 |
|
Nikolaj Bjorner
|
dea922ba25
|
fix #3909
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 13:56:07 -07:00 |
|
Nikolaj Bjorner
|
98ff388c4e
|
fix #3910
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 13:11:47 -07:00 |
|
Nikolaj Bjorner
|
b066f562c6
|
fix #3904
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 12:50:12 -07:00 |
|
Murphy Berzish
|
c1a0ce0862
|
Z3str3: reset internal data structures in init_search_eh() (#3818)
* z3str3: fixes to solver state between check-sat calls, wip
* z3str3: reset many internal data structures during init_search_eh() to clean up state
|
2020-04-11 12:36:30 -07:00 |
|
Nikolaj Bjorner
|
6ca039c855
|
fix #3919
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 12:31:38 -07:00 |
|
Lev Nachmanson
|
ec0cd644f1
|
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-11 12:28:54 -07:00 |
|
Lev Nachmanson
|
087354995d
|
roll back in find_beneficial_column_in_row_tableau_rows
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-11 12:24:22 -07:00 |
|
Lev Nachmanson
|
38c73090d8
|
avoid big pivots
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-04-11 11:49:58 -07:00 |
|
Arie Gurfinkel
|
20d72e5d97
|
(spacer) fix (get-proof) to return proper refutations
|
2020-04-11 14:38:27 -04:00 |
|
Nikolaj Bjorner
|
76c2fb5732
|
remove ref
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 11:36:19 -07:00 |
|
Arie Gurfinkel
|
1f6815213d
|
spacer: fail with exception on quantifiers in recursive rules
|
2020-04-11 14:16:47 -04:00 |
|
Arie Gurfinkel
|
1e96570365
|
fix #3915
|
2020-04-11 14:16:29 -04:00 |
|
Arie Gurfinkel
|
2b27aa1ce6
|
fix #3908
|
2020-04-11 13:58:10 -04:00 |
|
Arie Gurfinkel
|
f821ee38e5
|
Fix #3907
Protect spacer from existential quantifiers in the tail.
Some transformations seem to introduce existentially quantified terms.
|
2020-04-11 11:21:13 -04:00 |
|
Arie Gurfinkel
|
337c07a44c
|
Fix #3788 by converting assert into a throw
|
2020-04-11 09:15:32 -04:00 |
|
Nikolaj Bjorner
|
03e411c22d
|
fix #3868
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 02:28:38 -07:00 |
|
Nikolaj Bjorner
|
21a31fcd26
|
add missing fixed propagations on negated integer inequalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-11 02:28:38 -07:00 |
|
Arie Gurfinkel
|
ae5a713e81
|
fix #3906 by fixing a regression from today
|
2020-04-11 00:18:25 -04:00 |
|
Arie Gurfinkel
|
136b0b23ce
|
address #3905
|
2020-04-11 00:03:13 -04:00 |
|
Arie Gurfinkel
|
d53e30ecbe
|
finished fix for #3849 by converting assert into trace
|
2020-04-10 21:10:39 -04:00 |
|
Nikolaj Bjorner
|
fdabaa6cd2
|
fix #3807
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-04-10 13:43:00 -07:00 |
|
Arie Gurfinkel
|
fa900c39ab
|
hide fp.xform.scale
|
2020-04-10 15:46:59 -04:00 |
|