From 7a689c3298ea70d100eea427d3edc0d613c7cd73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Apr 2023 17:59:41 -0700 Subject: [PATCH] disable destructive equality resolution simplification if there are patterns - regression from F\star - reported by @mtzguido (stlc_min.smt2) --- src/ast/rewriter/th_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index d75a31a66..9278ae5ae 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -827,7 +827,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr_ref r(m()); bool der_change = false; - if (is_quantifier(result)) { + if (is_quantifier(result) && to_quantifier(result)->get_num_patterns() == 0) { m_der(to_quantifier(result), r, p2); der_change = result.get() != r.get(); if (m().proofs_enabled() && der_change)