3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Commit graph

14 commits

Author SHA1 Message Date
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07: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