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

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 28552ed79..ffcec7c0c 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -604,8 +604,12 @@ public:
   /**
    * Return a decision request, if the theory has one, or the NULL node
    * otherwise.
+   * If returning non-null node, hould set priority to
+   *                        0 if decision is necessary for model-soundness,
+   *                        1 if decision is necessary for completeness,
+   *                        >1 otherwise.
    */
-  virtual Node getNextDecisionRequest() { return Node(); }
+  virtual Node getNextDecisionRequest( unsigned& priority ) { return Node(); }
 
   /**
    * Statically learn from assertion "in," which has been asserted