Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.

2 files changed, 3 insertions, 2 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 28a08630e..7946fea59 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2119,10 +2119,11 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 }
 
 
-Node TheoryArrays::getNextDecisionRequest() {
+Node TheoryArrays::getNextDecisionRequest( unsigned& priority ) {
   if(! d_decisionRequests.empty()) {
     Node n = d_decisionRequests.front();
     d_decisionRequests.pop();
+    priority = 2;
     return n;
   } else {
     return Node::null();
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index c1223474c..77c5928f0 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -255,7 +255,7 @@ class TheoryArrays : public Theory {
   private:
   public:
 
-  Node getNextDecisionRequest();
+  Node getNextDecisionRequest( unsigned& priority );
 
   void presolve();
   void shutdown() { }