From daeab65ac6c6715a3e0c2f6fc0e61b1a7925b932 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 Aug 2019 12:01:27 -0500
Subject: [PATCH] Throw option exception when track inst lemmas is not used
 (#3145)

---
 src/theory/quantifiers/instantiate.cpp | 50 ++++++++++++++------------
 1 file changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 8bd39c241..7ecf9866a 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -644,42 +644,46 @@ void Instantiate::getExplanationForInstLemmas(
     std::map<Node, Node>& quant,
     std::map<Node, std::vector<Node> >& tvec)
 {
-  if (options::trackInstLemmas())
+  if (!options::trackInstLemmas())
   {
-    if (options::incrementalSolving())
+    std::stringstream msg;
+    msg << "Cannot get explanation for instantiations when --track-inst-lemmas "
+           "is false.";
+    throw OptionException(msg.str());
+  }
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
     {
-      for (std::pair<const Node, inst::CDInstMatchTrie*>& t :
-           d_c_inst_match_trie)
-      {
-        t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
-      }
+      t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
     }
-    else
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
     {
-      for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
-      {
-        t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
-      }
+      t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
     }
+  }
 #ifdef CVC4_ASSERTIONS
-    for (unsigned j = 0; j < lems.size(); j++)
-    {
-      Assert(quant.find(lems[j]) != quant.end());
-      Assert(tvec.find(lems[j]) != tvec.end());
-    }
-#endif
+  for (unsigned j = 0; j < lems.size(); j++)
+  {
+    Assert(quant.find(lems[j]) != quant.end());
+    Assert(tvec.find(lems[j]) != tvec.end());
   }
-  Assert(false);
+#endif
 }
 
 void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
 {
-  bool useUnsatCore = false;
-  std::vector<Node> active_lemmas;
-  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+  if (!options::trackInstLemmas())
   {
-    useUnsatCore = true;
+    std::stringstream msg;
+    msg << "Cannot get instantiations when --track-inst-lemmas is false.";
+    throw OptionException(msg.str());
   }
+  std::vector<Node> active_lemmas;
+  bool useUnsatCore = getUnsatCoreLemmas(active_lemmas);
 
   if (options::incrementalSolving())
   {
-- 
2.30.2