diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index f44397b9a..7d39b7611 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -44,7 +44,7 @@ void horner::lemmas_on_expr(nex& e) {
     cross_nested cn(e, [this](const nex& n) {
                         auto i = interval_of_expr(n);
                         m_intervals.check_interval_for_conflict_on_zero(i);} );
-    
+    cn.run();    
 }
 
 
diff --git a/src/math/lp/nla_expr.h b/src/math/lp/nla_expr.h
index f0d46c99e..c2582681e 100644
--- a/src/math/lp/nla_expr.h
+++ b/src/math/lp/nla_expr.h
@@ -119,7 +119,7 @@ public:
         case expr_type::MUL:
             return print_mul(out);
         case expr_type::VAR:
-            out << static_cast<char>('a'+m_j);
+            out << 'v' << m_j;
             return out;
         case expr_type::SCALAR:
             out << m_v;
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 840317496..98c2af258 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -72,7 +72,8 @@ void test_cn() {
     enable_trace("nla_cn");
     // (a(a+(b+c)c+d)d + e(a(e+c)+d)
     nex a = nex::var(0), b = nex::var(1), c = nex::var(2), d = nex::var(3), e = nex::var(4);
-    nex t = a*a*d + a*b*c*d + a*c*c*d + e*a*e + e*a*c + e*d;
+    nex t = a*a*d + a*b*c*d + a*c*c*d + a*d*d + e*a*e + e*a*c + e*d;
+    std::cout << "t = " << t << "\n";
     TRACE("nla_cn", tout << "t=" << t << '\n';);
     cross_nested cn(t, [](const nex& n) { std::cout << n << "\n"; } );
     cn.run();