3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-28 10:51:28 +00:00
Commit graph

11 commits

Author SHA1 Message Date
Nikolaj Bjorner
f4d256ef30 fix issue 153: assert rem/mod axiom no matter what is status of second argument
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-16 11:20:34 -08:00
Nikolaj Bjorner
d03a4bc306 check cancel flag after bcp. BCP returns in incomplete state after it check's the cancel flag. Propagate returns 'true' in this case so that the main loop exits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-02 14:33:42 -07:00
Nikolaj Bjorner
9412890c63 trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-26 12:58:55 -07:00
Nikolaj Bjorner
3ca8591347 take theory explanation into account
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-07-28 09:59:35 -07:00
Leonardo de Moura
8c211dd4fc Fix bug reported by Philippe Suter, see RELEASE_NOTES
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-17 14:07:21 -08:00
Leonardo de Moura
ffb7e26c75 removed front-end-params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 10:05:29 -08:00
Leonardo de Moura
288a96610f ported VCC trace streams
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 09:08:47 -08:00
Leonardo de Moura
02e763bb6b env params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 20:56:40 -08:00
Leonardo de Moura
9374a4e20a removed ini_file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 16:30:39 -08:00
Leonardo de Moura
e2f3f9abd7 removed dead code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-31 14:58:21 -07:00
Leonardo de Moura
add684d8e9 checkpoint
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-21 13:32:12 -07:00
Renamed from lib/smt_context.cpp (Browse further)