3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 08:21:56 +00:00
Commit graph

3 commits

Author SHA1 Message Date
Nikolaj Bjorner
67c4777514 fix #2548 fix #2530
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-09-13 15:03:04 +02:00
Arie Gurfinkel
1b83c677ea spacer: fixes lim_num_generalizer
Must check that newly constructed generalization blocks
the proof obligation.

Was only checking that generalization is entailed by the transition system!
2019-09-13 14:22:57 +02:00
Arie Gurfinkel
0d3fed9a6a spacer: lemma generalizer for small numbers
Attempts to reduce denominators in coefficients of farkas lemmas
2019-09-09 20:32:13 +02:00