1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index d8c69edac..5edd18464 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -1144,7 +1144,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
   }
 }
 
-bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
+bool SynthConjecture::getSynthSolutions(
+    std::map<Node, std::map<Node, Node> >& sol_map)
 {
   NodeManager* nm = NodeManager::currentNM();
   std::vector<Node> sols;
@@ -1153,6 +1154,8 @@ bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
   {
     return false;
   }
+  // we add it to the solution map, indexed by this conjecture
+  std::map<Node, Node>& smc = sol_map[d_quant];
   for (unsigned i = 0, size = d_embed_quant[0].getNumChildren(); i < size; i++)
   {
     Node sol = sols[i];
@@ -1182,7 +1185,7 @@ bool SynthConjecture::getSynthSolutions(std::map<Node, Node>& sol_map)
       Assert(fvar.getType().isComparableTo(bsol.getType()));
     }
     // store in map
-    sol_map[fvar] = bsol;
+    smc[fvar] = bsol;
   }
   return true;
 }