From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 10 Mar 2014 16:53:12 +0000 (-0500)
Subject: minor change for strings-fmf
X-Git-Tag: cvc5-1.0.0~7033
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a239cfbfdd81c65cf18b33df7bfcd6fb644b079;p=cvc5.git

minor change for strings-fmf
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index fd9605e59..64f3cd578 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -441,7 +441,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
 		  d_out->lemma(n_len_geq_zero);
 		  d_out->requirePhase( n_len_eq_z, true );
 		  // FMF
-		  if( n.getKind() == kind::VARIABLE ) {//options::stringFMF() &&
+		  if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
 			  d_input_vars.insert(n);
 		  }
 		}