diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index af0e356f0..1d00e30bd 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -127,7 +127,7 @@ void seq_axioms::add_extract_axiom(expr* e) {
     literal l_ge_0    = mk_ge(l, 0);
     literal l_le_0    = mk_le(l, 0);
     literal ls_le_0   = mk_le(ls, 0);
-    literal le_is_0   = mk_eq(le, 0);
+    literal le_is_0   = mk_eq(le, zero);
 
 
     // 0 <= i & i <= |s| & 0 <= l => xey = s