mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 03:48:51 +00:00
Code Activity

tweaks to string solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-28 17:16:46 -07:00
parent d5cf8e6263
commit 4cefa52497
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -446,6 +446,8 @@ namespace seq {
// |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
// ~contains(t,s) => indexof(t,s,offset) = -1
add_clause(mk_ge(i, -1));
add_clause(cnt, i_eq_m1);
add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);