From ce1c8ee9e34278893b57105be1167175c23f1ac9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Jul 2021 12:32:27 +0200 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index ba2e3a117..edc91e21f 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -820,7 +820,7 @@ namespace seq { /* * len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k} k > 1 * len(ubv2s(b)) = 1 => b < 10^{1} k = 1 - * len(ubv2s(b)) >= k => is_digit(nth(ubv2s(b),0) & ... & is_digit(nth(ubv2s(b),k-1) + * len(ubv2s(b)) >= k => is_digit(nth(ubv2s(b), 0)) & ... & is_digit(nth(ubv2s(b), k-1)) */ void axioms::ubv2s_len_axiom(expr* b, unsigned k) { expr_ref ge10k(m), ge10k1(m), eq(m), is_digit(m);