mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
disable unsound mk_seq_butlast
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ea0876b6d6
commit
11030fc81d
|
@ -943,7 +943,7 @@ expr_ref seq_rewriter::mk_seq_butlast(expr* t) {
|
|||
expr_ref result(m());
|
||||
expr* s, * j, * k;
|
||||
rational v;
|
||||
if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, v) && v.is_zero()) {
|
||||
if (false && str().is_extract(t, s, j, k) && m_autil.is_numeral(j, v) && v.is_zero()) {
|
||||
expr_ref_vector k_min_1(m());
|
||||
k_min_1.push_back(k);
|
||||
k_min_1.push_back(minus_one());
|
||||
|
|
Loading…
Reference in a new issue