diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 02:01:24 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:58 -0400 |
commit | 96eccb0d6134ccf4ead0134299b2e3750a890083 (patch) | |
tree | 2dc45e0c86337a1eafa049af42cc02e3743ef14a /contrib | |
parent | c8b948c37364104bf5f9ca5eca83120247b693a4 (diff) |
fix for sets/mar2014/..317minimized..
Observed behavior:
--check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.
Issue:
The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)
Resolution:
adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions