fix #4626

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · Aug 12, 2020 · 4045563 · 4045563
1 parent 5ecc59b
commit 4045563
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/smt/seq_offset_eq.cpp b/src/smt/seq_offset_eq.cpp
@@ -100,7 +100,7 @@ bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
     if (n1->get_owner_id() > n2->get_owner_id()) 
         std::swap(n1, n2);
     return 
-        !a.is_numeral(n2->get_owner()) && 
+        !a.is_numeral(n1->get_owner()) && 
         !a.is_numeral(n2->get_owner()) && 
         m_offset_equalities.find(n1, n2, offset);
 }