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

Merge pull request #8874 from Z3Prover/copilot/remove-unreachable-return-statement-another-one

Browse source 
Remove unreachable `return false` in `match_ubv2s1`
This commit is contained in:
Nikolaj Bjorner 2026-03-05 10:05:53 -08:00 • committed by GitHub
commit e9ee188747
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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) {