Florian Pigorsch
|
326bf401b9
|
Fix some spelling errors (mostly in comments).
|
2018-10-20 17:07:41 +02:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Bruce Mitchener
|
b7d1753843
|
Use override rather than virtual.
|
2018-02-09 21:19:27 +07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Nikolaj Bjorner
|
461e88e34c
|
additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-10-25 20:32:13 -07:00 |
|
Nikolaj Bjorner
|
5b497b6249
|
reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-22 20:25:47 -07:00 |
|
Christoph M. Wintersteiger
|
4e37821dde
|
"canceled" -> Z3_CANCELED_MSG
Relates to #431
|
2016-02-04 13:52:43 +00:00 |
|
Nikolaj Bjorner
|
baee4225a7
|
reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-11 16:21:24 -08:00 |
|
Nikolaj Bjorner
|
d9522cfd07
|
fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-06-23 12:05:19 +02:00 |
|
Nikolaj Bjorner
|
d32e4a9476
|
exposing facility to extract dependent clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-06-22 23:36:52 +02:00 |
|
Nikolaj Bjorner
|
ad0bdd7508
|
include statistics from sub-modules for QF_UFNRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-06-22 14:01:36 +02:00 |
|
Nikolaj Bjorner
|
564da787fb
|
add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-06-22 07:45:40 +02:00 |
|
Nikolaj Bjorner
|
c36df1c34a
|
fix openmp nested critical section
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
|
2015-05-18 12:43:55 -07:00 |
|
Nikolaj Bjorner
|
e8811748d3
|
fix regressions in nl/smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-16 19:08:37 +01:00 |
|
Nuno Lopes
|
6c22edc988
|
fix assorted compiler warnings
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
|
2015-05-16 11:44:58 +01:00 |
|
Nikolaj Bjorner
|
1a4e8f89bd
|
fix release build failure
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-10 14:53:05 -07:00 |
|
Nikolaj Bjorner
|
5063a2cdb6
|
add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-10 11:53:36 -07:00 |
|
Nikolaj Bjorner
|
6163085ff8
|
add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-10 10:02:44 -07:00 |
|
Nikolaj Bjorner
|
f5c048775b
|
add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-10 09:42:11 -07:00 |
|
Nikolaj Bjorner
|
c807ad0927
|
add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-09 21:28:26 -07:00 |
|
Nikolaj Bjorner
|
839e3fbb7c
|
add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-05-09 19:40:34 -07:00 |
|