aboutsummaryrefslogtreecommitdiff
path: root/src/infer/resolution.cc
diff options
context:
space:
mode:
Diffstat (limited to 'src/infer/resolution.cc')
-rw-r--r--src/infer/resolution.cc2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index 82e59b7..5fb0d4a 100644
--- a/src/infer/resolution.cc
+++ b/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