Nikolaj Bjorner
|
882c3bd0cd
|
fix unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-08-23 18:18:11 -03:00 |
|
Nikolaj Bjorner
|
491b3b34aa
|
tune consequence finding. Factor solver pretty-printing as SMT-LIB into top-level
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-08-03 11:14:29 -07:00 |
|
Nikolaj Bjorner
|
cb2d8d2107
|
add detection of non-fixed variables to consequence finding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-30 19:12:41 -07:00 |
|
Nikolaj Bjorner
|
d32019f4c9
|
fix consequence tracking for negated assumptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-30 10:49:06 -07:00 |
|
Nikolaj Bjorner
|
2263be1b4d
|
adding consequence examples
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-29 17:24:14 -07:00 |
|
Nikolaj Bjorner
|
5c99405db3
|
finish consequence fast path code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-28 20:15:47 -07:00 |
|
Nikolaj Bjorner
|
4958edeb42
|
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-28 19:40:49 -07:00 |
|
Nikolaj Bjorner
|
8221a09659
|
fast path for antecedent extraction in smt_context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-07-28 16:49:19 -07:00 |
|