3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 09:56:39 +00:00
Commit graph

8 commits

Author SHA1 Message Date
Leonardo de Moura
2cc3e3745e Fix gcc compilation error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-02 21:14:22 -08:00
Nikolaj Bjorner
d318aab7d1 experiments wtih QHC
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2013-01-02 09:49:27 -08:00
Nikolaj Bjorner
63b7f7ecd6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2012-12-28 16:40:36 -08:00
Nikolaj Bjorner
9f2743309f fix to proof hypothesis removal facility reported by Arie Gurfinkel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-28 16:40:29 -08:00
Leonardo de Moura
d92efeb0c5 Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-18 17:14:25 -08:00
Nikolaj Bjorner
639f902ad1 fix bug in difference logic recognizer, assert in proof_util
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-12-11 17:01:00 -08:00
Nikolaj Bjorner
29a45e34a2 fixing bugs in model evaluator. remove wrong assertions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2012-11-17 22:09:15 +01: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/proof_utils.cpp (Browse further)