Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
	src/theory/strings/theory_strings_preprocess.cpp

diff --cc src/theory/strings/theory_strings_preprocess.cpp
index 04e7a06cc6409105e982cfb4c082fceee4d394bf,6520f551755d52386e0ea99329c9f7a2c9b20d51..1df79ccff1af85745b6e3a0276d7b38e7c2987a1
--- 1/src/theory/strings/theory_strings_preprocess.cpp
--- 2/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@@ -238,11 -236,6 +238,11 @@@ Node StringsPreprocess::simplify( Node 
                        Node pret = NodeManager::currentNM()->mkNode(kind::STRING_ITOS, num);
                        Node lenp = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, pret);
  
-                       Node lem = NodeManager::currentNM()->mkNode(kind::IFF,
++                      /*Node lem = NodeManager::currentNM()->mkNode(kind::IFF,
 +                              t.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))),
 +                              t[0].eqNode(d_zero));
-                       new_nodes.push_back(lem);
++                      new_nodes.push_back(lem);*/
 +
                        Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
                        Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
                        Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ),
@@@ -276,10 -269,6 +276,10 @@@
                        Node lstx = lenp.eqNode(NodeManager::currentNM()->mkNode(kind::PLUS, b1, one));
                        Node cc2 = ufx.eqNode(ufMx);
                        cc2 = NodeManager::currentNM()->mkNode(kind::IMPLIES, lstx, cc2);
-                       Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(t[0]).negate());
 +                      // leading zero
++                      Node cl = NodeManager::currentNM()->mkNode(kind::AND, lstx, d_zero.eqNode(b1).negate());
 +                      Node cc21 = NodeManager::currentNM()->mkNode(kind::IMPLIES, cl, NodeManager::currentNM()->mkNode(kind::GT, ufMx, d_zero));
 +                      //cc3
                        Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
                        Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);