mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 05:44:51 +00:00
Code Activity

Remove unreachable return false in match_ubv2s1

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-05 17:58:13 +00:00
parent 40c5c7a5b7
commit 870ba21b84
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_eq_solver.cpp
View file

@ -226,7 +226,6 @@ namespace seq {
return
e.ls.size() == 1 && e.rs.size() == 1 &&
seq.str.is_ubv2s(e.ls[0], a) && seq.str.is_ubv2s(e.rs[0], b);
return false;
}
bool eq_solver::reduce_ubv2s1(eqr const& e, eq_ptr& r) {