diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp
index 15eab50b9..89c662822 100644
--- a/src/ast/ast_util.cpp
+++ b/src/ast/ast_util.cpp
@@ -373,7 +373,4 @@ static app_ref plus(ast_manager& m, expr* a, int i) {
     return app_ref(arith.mk_add(a, arith.mk_int(i)), m);
 }
 
-app_ref operator+(expr_ref& a, expr* b) { return plus(a.m(), a, b); }
-app_ref operator+(app_ref& a, expr* b) { return plus(a.m(), a, b); }
-app_ref operator+(expr_ref& a, int i) { return plus(a.m(), a, i); }
-app_ref operator+(app_ref& a, int i) { return plus(a.m(), a, i); }
+app_ref operator+(expr_ref& a, expr_ref& b) { return plus(a.m(), a, b); }
diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h
index fe4bde465..58cfa48b9 100644
--- a/src/ast/ast_util.h
+++ b/src/ast/ast_util.h
@@ -120,10 +120,7 @@ inline app_ref operator|(expr_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b
 inline app_ref operator|(app_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
 inline app_ref operator|(var_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
 inline app_ref operator|(quantifier_ref& a,  expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); }
-app_ref operator+(expr_ref& a, expr* b);
-app_ref operator+(app_ref& a, expr* b);
-app_ref operator+(expr_ref& a, int i);
-app_ref operator+(app_ref& a, int i);
+app_ref operator+(expr_ref& a, expr_ref& b);
 
 /**
    Return (or args[0] ... args[num_args-1]) if num_args >= 2
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 51b0186e2..3ed16592d 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -35,8 +35,7 @@ Q: Is this sufficient? Axiom A1 could be adjusted to add new elements i' until t
 This is quite bad when k is very large. Instead rely on stably infiniteness or other domain properties of the theories.
 
 When A is finite domain, or there are quantifiers there could be constraints that force domain sizes so domain sizes may have 
-to be enforced. A succinct way would be through domain comprehension assertions. Thus, if we have 
-S[i1],.., S[ik], !S[j1],...,!S[jl] asserted on integer domain i, then 
+to be enforced. A succinct way would be through domain comprehension assertions. 
 
 Finite domains:
 
@@ -53,6 +52,8 @@ Finite domains:
     ---------------------------------------------------------------
                      Size(S, n) n fresh.
 
+    Model construction for infinite domains when all Size(S, m) are negative for S.
+
  */
 
 #include "ast/ast_util.h"