diff options
| author | Tim King <taking@google.com> | 2016-12-29 15:43:04 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2016-12-29 15:43:04 -0800 |
| commit | b8b51a0c359628d7202a8a5ff0c2a4beb4c041e9 (patch) | |
| tree | 10a0d5b6cc7df2a27f3ffe7df95c0d542f4162ed /src/theory/bv | |
| parent | d7fba3b8370daa65f368b5982041f53252b6428c (diff) | |
Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 5fbdf74ab..617e3b761 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -47,8 +47,8 @@ class InequalitySolver: public SubtheorySolver { InequalityGraph d_inequalityGraph; context::CDHashMap<Node, TNode, NodeHashFunction> d_explanations; context::CDO<bool> d_isComplete; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - TNodeSet d_ineqTerms; + typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; + NodeSet d_ineqTerms; bool isInequalityOnly(TNode node); bool addInequality(TNode a, TNode b, bool strict, TNode fact); Statistics d_statistics; |