From 99c90d2419e0e3c40e467080d40f13952a81b7a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 18 Apr 2020 19:46:23 -0700 Subject: [PATCH] fix crash Signed-off-by: Nikolaj Bjorner --- src/smt/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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