3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 18:06:40 +00:00
Commit graph

7 commits

Author SHA1 Message Date
Johannes Kanig
9bfa73ee06 Take into account number of monomials for rlimit counting
Should fix issue #611
2016-06-08 11:17:26 +09:00
Nikolaj Bjorner
5e7db2e3e2 disable mk_array_eq as it breaks model evaluation/validation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-18 08:29:24 -07:00
Nikolaj Bjorner
42726171b5 add limit checks in Grobner. Issue #599
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-05-15 11:34:48 -07:00
Nikolaj Bjorner
6b82b949cf Make Groebner basis computation interruptable. Exponsed in issue #269
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-28 11:39:59 -07:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-31 14:45:10 -07:00
Nikolaj Bjorner
7c9dd6b8a8 fix exception unsafety leading to double free, issues #184 and issue #175. Location and fix strategy suggested by Nuno
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-09 00:34:59 +02:00
Leonardo de Moura
9e299b88c4 reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-23 21:53:34 -07:00
Renamed from src/grobner/grobner.cpp (Browse further)