1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 889f4d9c9..8050e97f8 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -364,12 +364,12 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
     // are not passive
     return Node::null();
   }
-  e = d_tds->getSynthFunForEnumerator(e);
+  Node ee = d_tds->getSynthFunForEnumerator(e);
   Assert(!e.isNull());
-  std::map<Node, bool>::iterator itx = d_examples_invalid.find(e);
+  std::map<Node, bool>::iterator itx = d_examples_invalid.find(ee);
   if (itx == d_examples_invalid.end()) {
-    unsigned nex = d_examples[e].size();
-    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, e, bvr, this, 0, nex);
+    unsigned nex = d_examples[ee].size();
+    Node ret = d_pbe_trie[e][tn].addPbeExample(tn, ee, bvr, this, 0, nex);
     Assert(ret.getType() == bvr.getType());
     return ret;
   }