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, 2 insertions, 1 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index c8b41c035..7f36f4d25 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -154,6 +154,7 @@ private:
   Node getModelTerm( Node n );
 public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
+  ~CegInstantiation();
 public:
   bool needsCheck( Theory::Effort e );
   unsigned needsModel( Theory::Effort e );
@@ -163,7 +164,7 @@ public:
   void preRegisterQuantifier( Node q );
   void registerQuantifier( Node q );
   void assertNode( Node n );
-  Node getNextDecisionRequest();
+  Node getNextDecisionRequest( unsigned& priority );
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   std::string identify() const { return "CegInstantiation"; }
   /** print solution for synthesis conjectures */