mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Merge pull request #8694 from Z3Prover/copilot/sub-pr-8686

Browse source 
Fix ambiguous svector constructor calls in theory_finite_set_lattice_refutation
This commit is contained in:
Nikolaj Bjorner 2026-02-19 10:49:13 -08:00 • committed by GitHub
commit 44cd412426
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_finite_set_lattice_refutation.cpp
View file

@ -19,10 +19,10 @@ const int MAX_DECISION_LITERALS = 10;
namespace smt { namespace smt {
reachability_matrix::reachability_matrix(context &ctx, theory_finite_set_lattice_refutation &t_lattice) reachability_matrix::reachability_matrix(context &ctx, theory_finite_set_lattice_refutation &t_lattice)
: reachable(NUM_WORDS * NUM_WORDS * 64, 0ull), : reachable(NUM_WORDS * NUM_WORDS * 64, (uint64_t)0),
links(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}), links(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}),
link_dls(NUM_WORDS * NUM_WORDS * 64 * 64, 0ull), link_dls(NUM_WORDS * NUM_WORDS * 64 * 64, (uint64_t)0),
non_links(NUM_WORDS * NUM_WORDS * 64, 0ull), non_links(NUM_WORDS * NUM_WORDS * 64, (uint64_t)0),
non_link_justifications(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}), non_link_justifications(NUM_WORDS * NUM_WORDS * 64 * 64, {nullptr, nullptr}),
largest_var(0), largest_var(0),
max_size(NUM_WORDS * 64), max_size(NUM_WORDS * 64),