From: Tianyi Liang Date: Mon, 10 Mar 2014 16:53:12 +0000 (-0500) Subject: minor change for strings-fmf X-Git-Tag: cvc5-1.0.0~7032^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1812b11229884378fef6891e74c7c17cf9bafdd;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); } }