2 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5a99f8e30..ade5428ca 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3802,7 +3802,7 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) {
 
 //// Finite Model Finding
 
-Node TheoryStrings::getNextDecisionRequest() {
+Node TheoryStrings::getNextDecisionRequest( unsigned& priority ) {
   if( options::stringFMF() && !d_conflict ){
     Node in_var_lsum = d_input_var_lsum.get();
     //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
@@ -3852,6 +3852,7 @@ Node TheoryStrings::getNextDecisionRequest() {
         }
         Node lit = d_cardinality_lits[ decideCard ];
         Trace("strings-fmf") << "Strings::FMF: Decide positive on " << lit << std::endl;
+        priority = 1;
         return lit;
       }
     }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 6665f9e50..457afb15a 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -502,7 +502,7 @@ private:
   context::CDO< int > d_curr_cardinality;
 public:
   //for finite model finding
-  Node getNextDecisionRequest();
+  Node getNextDecisionRequest( unsigned& priority );
   //ppRewrite
   Node ppRewrite(TNode atom);
 public: