From 512aa2a9e6f354bd6df866592ca8acec49631a97 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 12:47:03 -0700
Subject: [PATCH] fix #3609
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/arith_eq_adapter.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp
index 593eb1d71..bc381b822 100644
--- a/src/smt/arith_eq_adapter.cpp
+++ b/src/smt/arith_eq_adapter.cpp
@@ -212,7 +212,7 @@ namespace smt {
if (m_params.m_arith_add_binary_bounds) {
TRACE("arith_eq_adapter", tout << "adding binary bounds...\n";);
- ctx.mk_th_axiom(tid, le_lit, ge_lit, 3, m_proof_hint.c_ptr());
+ ctx.mk_th_axiom(tid, le_lit, ge_lit, m_proof_hint.size(), m_proof_hint.c_ptr());
}
if (ctx.relevancy()) {
relevancy_eh * eh = ctx.mk_relevancy_eh(arith_eq_relevancy_eh(n1->get_owner(), n2->get_owner(), t1_eq_t2, le, ge));