diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
| commit | a26a9311ed6cc34860092252d1750428b741b116 (patch) | |
| tree | 83eb5ccd5e94100a8e0368e8f25c977a2e2e6c03 /proofsearch/src/infer/resolution.cc | |
| parent | 598f364de0a809747714294326a0193788e0bdfb (diff) | |
| download | rcc-project-a26a9311ed6cc34860092252d1750428b741b116.tar.gz rcc-project-a26a9311ed6cc34860092252d1750428b741b116.tar.xz | |
feat: enhance clang-tidy configuration and improve code quality across multiple files
Diffstat (limited to 'proofsearch/src/infer/resolution.cc')
| -rw-r--r-- | proofsearch/src/infer/resolution.cc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc index 82e59b7..5fb0d4a 100644 --- a/proofsearch/src/infer/resolution.cc +++ b/proofsearch/src/infer/resolution.cc @@ -98,7 +98,7 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, // Rename c2's variables to avoid clashes with c1 // Use a static counter — safe for single-threaded prover static uint32_t var_counter = 0; - auto& symbols = const_cast<SymbolTable&>(bank.symbols()); + auto& symbols = bank.mutableSymbols(); Clause c2r = renameVariables(c2, bank, symbols, var_counter); // Unify the complementary atoms |