From 72d129eb75c4b9a8e30b2428fd90e6e9f58e0dfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 May 2020 13:13:09 -0700 Subject: [PATCH] #4396 Signed-off-by: Nikolaj Bjorner --- src/smt/arith_eq_adapter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 50b6aa4e2..2777c82ce 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -81,7 +81,8 @@ namespace smt { }; void arith_eq_adapter::mk_axioms(enode * n1, enode * n2) { - SASSERT(n1 != n2); + if (n1 == n2) + return; ast_manager & m = get_manager(); TRACE("arith_eq_adapter_mk_axioms", tout << "#" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n"; tout << mk_ismt2_pp(n1->get_owner(), m) << "\n" << mk_ismt2_pp(n2->get_owner(), m) << "\n";);