mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

#7255 #7328

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-03 09:37:14 -07:00
parent d6040ee5ab
commit bc8fa67afc
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -1117,6 +1117,8 @@ namespace smt {
*/ */
bool context::is_diseq(enode * n1, enode * n2) const { bool context::is_diseq(enode * n1, enode * n2) const {
SASSERT(n1->get_sort() == n2->get_sort()); SASSERT(n1->get_sort() == n2->get_sort());
if (m.are_distinct(n1->get_expr(), n2->get_expr()))
return true;
context * _this = const_cast<context*>(this); context * _this = const_cast<context*>(this);
if (!m_is_diseq_tmp) { if (!m_is_diseq_tmp) {
app * eq = m.mk_eq(n1->get_expr(), n2->get_expr()); app * eq = m.mk_eq(n1->get_expr(), n2->get_expr());