mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-30 23:53:44 +00:00
Code Activity

Apply code simplification improvements

Browse source 
- Consolidated two contains() methods into single template function
- Added const correctness to helper methods in argument_parser.h
- Improved string handling (replaced substr with compare, return "" instead of std::string())
- Fixed indentation in nlsat_solver.cpp nested loop
- Modernized empty container return syntax in lp.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-12 02:59:21 +00:00
parent 160b98786f
commit bb177988eb
3 changed files with 13 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_solver.cpp
View file

@ -1208,8 +1208,8 @@ namespace nlsat {
used_bools[b] = true;
vars.reset();
this->vars(lit, vars);
for (var v : vars)
used_vars[v] = true;
for (var v : vars)
used_vars[v] = true;
}
display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
if (m_log_lemma_smtrat)