fix for sets/mar2014/..317minimized..
authorKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 20 Mar 2014 06:01:24 +0000 (02:01 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Thu, 20 Mar 2014 21:18:58 +0000 (17:18 -0400)
commit96eccb0d6134ccf4ead0134299b2e3750a890083
tree2dc45e0c86337a1eafa049af42cc02e3743ef14a
parentc8b948c37364104bf5f9ca5eca83120247b693a4
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().
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/theory_model.cpp
test/regress/regress0/sets/Makefile.am
test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2 [new file with mode: 0644]
test/regress/regress0/sets/mar2014/sharing-preregister.smt2 [new file with mode: 0644]