diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-22 20:06:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 20:06:42 -0500 |
| commit | 56f2e6dc41fa5fbeff1755978fa1854e800846b5 (patch) | |
| tree | a80823831c0f032fe769d518afa48f5cf3e2f3f4 /src/smt | |
| parent | 115511f6c5732cac1c3718d365d1cf5596541c95 (diff) | |
Fix type issue with term formula removal (#5107)
We currently are using lookups with uint32_t but storing with int32_t. Somehow the compilers don't complain, but I noticed this was mismatched.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/term_formula_removal.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index e7a61d953..30972c1cc 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -121,9 +121,9 @@ class RemoveTermFormulas { private: typedef context::CDInsertHashMap< - std::pair<Node, int32_t>, + std::pair<Node, uint32_t>, Node, - PairHashFunction<Node, int32_t, NodeHashFunction> > + PairHashFunction<Node, uint32_t, NodeHashFunction> > TermFormulaCache; /** term formula removal cache * |