From 30d1800c3176b6bd6ca5a3e2c6109ad96784ba18 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Sep 2023 10:32:51 -0700 Subject: [PATCH] #6916 short circuiting equality consequence appears to have the wrong sign --- src/smt/smt_consequences.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 657e222da..cac8d40b1 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -243,7 +243,7 @@ namespace smt { lit.neg(); literal lit = mk_diseq(k, v); - literals.push_back(lit); + literals.push_back(~lit); mk_clause(literals.size(), literals.data(), nullptr); TRACE("context", display_literals_verbose(tout, literals.size(), literals.data());); }