From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Mon, 31 Mar 2014 22:33:35 +0000 (-0500)
Subject: minor typo/bug fix
X-Git-Tag: cvc5-1.0.0~6991^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=68f0639316daf5dfe362febe66cafe258aad5073;p=cvc5.git

minor typo/bug fix
---

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6981a2a33..3167734ee 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -424,7 +424,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
 			Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
 			Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
 						NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
-						NodeManager::currentNM()->mkNode(kind::GT, pret, b2));
+						NodeManager::currentNM()->mkNode(kind::GT, lenp, b2));
 			Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
 			Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
 			Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);