From 1589592be3c93ab2c3d42b9875535f950fe6b982 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 May 2018 19:55:47 -0500
Subject: [PATCH] Fix (#1979)

---
 src/theory/quantifiers/sygus/term_database_sygus.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index cd6c8bdec..8f20e2ffc 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -817,6 +817,7 @@ void TermDbSygus::registerEnumerator(Node e,
     d_enum_to_active_guard[e] = eg;
   }
 
+  d_enum_to_using_sym_cons[e] = useSymbolicCons;
   // depending on if we are using symbolic constructors, introduce symmetry
   // breaking lemma templates for each relevant subtype of the grammar
   std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
-- 
2.30.2