From 1b1ebaa3b03703cc76131e66c7cf9631685bf0ed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 3 Dec 2023 12:43:39 -0800
Subject: [PATCH] minor simplification during internalization
---
src/sat/smt/arith_solver.h | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 84be3caa7..20ae599c2 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -292,10 +292,11 @@ namespace arith {
theory_var internalize_linearized_def(expr* term, scoped_internalize_state& st);
void init_left_side(scoped_internalize_state& st);
bool internalize_term(expr* term);
- bool internalize_atom(expr* atom);
+ bool internalize_atom(expr* atom);
bool is_unit_var(scoped_internalize_state& st);
bool is_one(scoped_internalize_state& st);
bool is_zero(scoped_internalize_state& st);
+ expr* mk_sub(expr* a, expr* b);
enode* mk_enode(expr* e);
lpvar register_theory_var_in_lar_solver(theory_var v);