mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 08:44:10 +00:00
Code Activity

Removed unused function

Browse source
This commit is contained in:
CEisenhofer 2026-04-13 15:05:41 +02:00
parent d620f20c63
commit 9155ce85bb
2 changed files with 0 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4125,11 +4125,6 @@ namespace seq {
return exp_snode ? exp_snode->get_expr() : nullptr;
}
expr_ref nielsen_graph::mk_fresh_int_var() {
std::string name = "n!" + std::to_string(m_fresh_cnt++);
return expr_ref(m.mk_fresh_const(name.c_str(), a.mk_int()), m);
}
// -----------------------------------------------------------------------
// Regex widening: overapproximate string and check intersection emptiness
// Mirrors ZIPT NielsenNode.CheckRegexWidening (NielsenNode.cs:1350-1380)

3
src/smt/seq/seq_nielsen.h
View file

@ -1141,9 +1141,6 @@ namespace seq {
// get the exponent expression from a power snode (arg(1))
expr* get_power_exponent(euf::snode* power);
// create a fresh integer variable expression (for power exponents)
expr_ref mk_fresh_int_var();
// -----------------------------------------------
// Modification counter methods for substitution length tracking.
// mirrors ZIPT's NielsenEdge.IncModCount / DecModCount and