From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 23 Sep 2020 01:06:42 +0000 (-0500)
Subject: Fix type issue with term formula removal (#5107)
X-Git-Tag: cvc5-1.0.0~2820
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=56f2e6dc41fa5fbeff1755978fa1854e800846b5;p=cvc5.git

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.
---

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
    *