minor typo/bug fix

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6981a2a33754e3a7c6c41dda6e7061b1385b87a9..3167734ee4a987203b1298d23383f50c381ccde8 100644 (file)
--- 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);