From a4f4975092030837f3e6bb2a8df162771dc6494c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 Jul 2021 21:08:53 +0200
Subject: [PATCH] #5336
---
src/sat/smt/q_ematch.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index da7e670c8..e997476ed 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -401,7 +401,12 @@ namespace q {
for (expr* arg : ors) {
bool sign = m.is_not(arg, arg);
expr* l, *r;
- if (!m.is_eq(arg, l, r) || is_ground(arg)) {
+ if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
+ l = to_app(arg)->get_arg(0);
+ r = to_app(arg)->get_arg(1);
+ sign = !sign;
+ }
+ else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
l = arg;
r = sign ? m.mk_false() : m.mk_true();
sign = false;