fix crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 19, 2020 · 99c90d2 · 99c90d2
1 parent 0fe2d3d
commit 99c90d2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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