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

1 files changed, 8 insertions, 5 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 95b01bc7b..22bfa948f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -767,14 +767,17 @@ void QuantifiersEngine::propagate( Theory::Effort level ){
   }
 }
 
-Node QuantifiersEngine::getNextDecisionRequest(){
+Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
+  unsigned min_priority;
+  Node dec;  
   for( unsigned i=0; i<d_modules.size(); i++ ){
-    Node n = d_modules[i]->getNextDecisionRequest();
-    if( !n.isNull() ){
-      return n;
+    Node n = d_modules[i]->getNextDecisionRequest( priority );
+    if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
+      dec = n;
+      min_priority = priority;
     }
   }
-  return Node::null();
+  return dec;
 }
 
 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {