From 68f0639316daf5dfe362febe66cafe258aad5073 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Mon, 31 Mar 2014 17:33:35 -0500 Subject: [PATCH] minor typo/bug fix --- src/theory/strings/theory_strings_preprocess.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); -- 2.30.2