summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-08-14 22:46:48 -0700
committerGitHub <noreply@github.com>2017-08-14 22:46:48 -0700
commit6432a16bd86c7540dad4ce5321ee68b7a7287c66 (patch)
tree4855efd77237c767a8a94f063e1f521d2b452ac0 /src/expr/mkexpr
parent779ca55f2802b2c77ea39d1c94a097a9761f544c (diff)
Minimize includes in expr.h: remove dups, iostream (#219)
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-xsrc/expr/mkexpr6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 60ee758d8..010ec9a2e 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -218,8 +218,12 @@ function constant {
lineno=${BASH_LINENO[0]}
check_theory_seen
- includes="${includes}
+ # Only add include if it is not in the list of includes yet
+ if [[ "${includes}" != *"#include \"$4\""* ]]; then
+ includes="${includes}
#include \"$4\""
+ fi
+
mkConst_instantiations="${mkConst_instantiations}
#line $lineno \"$kf\"
template <> Expr ExprManager::mkConst($2 const& val);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback