mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-18 19:14:29 +00:00
Code Activity

Add safety cap on minterm computation and assertion for invariant

Browse source 
Co-authored-by: NikolajBjorner <56730610+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-02 19:29:41 +00:00
parent 150f1fe2ea
commit 1274a1e3c0
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_sgraph.cpp
View file

@ -477,6 +477,9 @@ namespace euf {
// generate minterms as conjunctions/negations of predicates
// for n predicates, there are up to 2^n minterms
unsigned n = preds.size();
// cap at reasonable size to prevent exponential blowup
if (n > 20)
n = 20;
for (unsigned mask = 0; mask < (1u << n); ++mask) {
expr_ref_vector conj(m);
for (unsigned i = 0; i < n; ++i) {
@ -485,6 +488,7 @@ namespace euf {
else
conj.push_back(m_seq.re.mk_complement(preds.get(i)));
}
SASSERT(!conj.empty());
// intersect all terms
expr_ref mt(conj.get(0), m);
for (unsigned i = 1; i < conj.size(); ++i)