From 4628cb8e794521ed37b49ce7177a1cb34f496a06 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Jul 2020 11:30:35 -0700
Subject: [PATCH] check for negation, not complement
---
src/ast/rewriter/seq_rewriter.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 708ec1978..528c84502 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -2493,8 +2493,8 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) {
unsigned ch;
if (u().is_char_le(e, ch1, ch2) && u().is_const_char(ch2, ch))
return ch;
- // Fallback: use expression ID (but use same ID for complement)
- re().is_complement(e, e);
+ // Fallback: use expression ID (but use same ID for negation)
+ m().is_not(e, e);
return e->get_id();
};
if (m().is_ite(a, ca, a1, a2)) {