diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-01 14:57:25 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-01 16:57:25 -0600 |
| commit | ac9808bdc0c6d5619f636691bd737079b50b9ea5 (patch) | |
| tree | 992c9b9ef1de1d7539856cd2e761269020ddf085 /test/unit | |
| parent | 9bf87b8b5572bbfc110018081b28ad0a88b8a619 (diff) | |
Prevent ref count from reaching zero in BV instantiator (#3512)
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_instantiator_white.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 2b61aeb00..0fa7a3f82 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -153,7 +153,7 @@ void BvInstantiatorWhite::testNormalizePvMult() Node zero = mkZero(32); Node one = mkOne(32); BvLinearAttribute is_linear; - std::unordered_map<TNode, bool, TNodeHashFunction> contains_x; + std::unordered_map<Node, bool, NodeHashFunction> contains_x; contains_x[x] = true; contains_x[neg_x] = true; @@ -251,7 +251,7 @@ void BvInstantiatorWhite::testNormalizePvPlus() Node c = mkVar(32); Node d = mkVar(32); BvLinearAttribute is_linear; - std::unordered_map<TNode, bool, TNodeHashFunction> contains_x; + std::unordered_map<Node, bool, NodeHashFunction> contains_x; contains_x[x] = true; contains_x[neg_x] = true; @@ -374,7 +374,7 @@ void BvInstantiatorWhite::testNormalizePvEqual() Node one = mkOne(32); Node ntrue = mkTrue(); BvLinearAttribute is_linear; - std::unordered_map<TNode, bool, TNodeHashFunction> contains_x; + std::unordered_map<Node, bool, NodeHashFunction> contains_x; contains_x[x] = true; contains_x[neg_x] = true; |