From 372696096944940bc35a12a27f186be0bfe76b60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 29 Oct 2023 17:43:53 -0700
Subject: [PATCH] fix #6969
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 4 ----
1 file changed, 4 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 132f51693..df59537b5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -589,15 +589,11 @@ class theory_lra::imp {
void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";);
-// static unsigned num_bin = 0;
-// std::cout << "binary " << (num_bin++) << "\n";
ctx().mk_th_lemma(get_id(), l1, l2, num_params, params);
}
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; ctx().display_literals_smt2(tout, 3, lits); tout << "\n";);
- static unsigned num_ter = 0;
- std::cout << "ternary " << (num_ter++) << "\n";
ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params);
}