mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

Add clarifying comment to m_str_eq.empty() postcondition

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/24442582-8437-45ae-a58f-957ac2bdf698

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-03 02:12:35 +00:00 • committed by GitHub
parent 0726edcd0a
commit a4cfbfa274
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/seq/seq_nielsen.cpp
View file

@ -1207,6 +1207,8 @@ namespace seq {
if (is_satisfied()) {
// pass 1 removed all trivial str_eq entries; is_satisfied() requires
// the remainder to be trivial, so the vector must be empty here.
SASSERT(m_str_eq.empty());
return simplify_result::satisfied;
}