mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 21:38:44 +00:00
fresh index
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c92a63690d
commit
ce4e1d3cbb
|
@ -77,7 +77,7 @@ namespace smt {
|
|||
ts.push_back(mk_cont(idx));
|
||||
for (auto const& p : patterns) {
|
||||
ts.append(p);
|
||||
ts.push_back(mk_cont(idx));
|
||||
ts.push_back(mk_cont(++idx));
|
||||
}
|
||||
t = th.mk_concat(ts, seq_sort);
|
||||
th.propagate_eq(lit, s, t, true);
|
||||
|
|
Loading…
Reference in a new issue