mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix typos in comments

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-26 15:14:39 -07:00
parent a1b036a4fa
commit 22a76e4985
2 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/seq_axioms.cpp
View file

@ -437,7 +437,7 @@ namespace seq {
expr_ref t_eq_empty = mk_eq_empty(t);
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
// ~contains(t,s) <=> indexof(t,s,offset) = -1
// ~contains(t,s) => indexof(t,s,offset) = -1
add_clause(cnt, i_eq_m1);
add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
@ -489,7 +489,7 @@ namespace seq {
// 0 <= offset & offset < len(t) => len(x) = offset
// 0 <= offset & offset < len(t) & indexof(y,s,0) = -1 => -1 = i
// 0 <= offset & offset < len(t) & indexof(y,s,0) >= 0 =>
// -1 = indexof(y,s,0) + offset = indexof(t, s, offset)
// indexof(y,s,0) + offset = indexof(t, s, offset)
add_clause(~offset_ge_0, offset_ge_len, mk_seq_eq(t, mk_concat(x, y)));
add_clause(~offset_ge_0, offset_ge_len, mk_eq(mk_len(x), offset));