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:39:19 -07:00
parent bc8fa67afc
commit 52f8eb21fb
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.cpp
View file

@ -1117,7 +1117,7 @@ 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())) if (m.are_distinct(n1->get_root()->get_expr(), n2->get_root()->get_expr()))
return true; return true;
context * _this = const_cast<context*>(this); context * _this = const_cast<context*>(this);
if (!m_is_diseq_tmp) { if (!m_is_diseq_tmp) {