diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 00:31:22 -0400 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-04-11 00:31:49 -0400 |
| commit | 3dc1ba4ef7630e8bed64a5d2fc8843611ad4dd1f (patch) | |
| tree | 71b4a18442c15f1525b7815e02058d36c12dbc19 /src/theory/arrays/theory_arrays.h | |
| parent | 5684cdec81cee9a29958388e1980b369a48b05bb (diff) | |
Added check for infinite lemma loop
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 39fd90012..2a0083823 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -358,6 +358,7 @@ class TheoryArrays : public Theory { // List of nodes that need permanent references in this context context::CDList<Node> d_permRef; context::CDList<Node> d_modelConstraints; + context::CDList<Node> d_lemmasSaved; std::vector<Node> d_lemmas; Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); |