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

Fix str.< Skolem length generation overhead

Browse source
This commit is contained in:
CEisenhofer 2026-04-04 18:32:02 +02:00
parent b60a44c66b
commit a58a9114d2
2 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_nseq.cpp
View file

@ -175,6 +175,9 @@ namespace smt {
// register in our private sgraph
get_snode(term);
if (m_seq.is_seq(term) && m_axioms.sk().is_skolem(term))
ensure_length_var(term);
// track higher-order terms for lazy unfolding
expr* ho_f = nullptr, *ho_s = nullptr, *ho_b = nullptr, *ho_i = nullptr;
if (m_seq.str.is_map(term, ho_f, ho_s) ||

1
src/smt/theory_nseq.h
View file

@ -19,7 +19,6 @@ Author:
--*/
#pragma once
#include <variant>
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/seq_axioms.h"