diff --git a/include/lustrec_math.lusi b/include/lustrec_math.lusi
index aef61c940e3c3a7c36ef194a5ae229e50fb9d33c..9eadabb8080ac63d17dd1489c95b90df346f5cc0 100644
--- a/include/lustrec_math.lusi
+++ b/include/lustrec_math.lusi
@@ -23,4 +23,4 @@ function sinh (x: real) returns (y: real) prototype C lib m;
 function sqrt (x: real) returns (y: real) prototype C lib m;
 function trunc (x: real) returns (y: real) prototype C lib m;
 function tan (x: real) returns (y: real) prototype C lib m;
-
+function tanh (x: real) returns (y: real) prototype C lib m;
diff --git a/include/lustrec_math.smt2 b/include/lustrec_math.smt2
index 91c3a4dea48843f327df5130f3f290b867e1cfca..86e58817044b93d1bf35b3b3fb89102b5c32c878 100644
--- a/include/lustrec_math.smt2
+++ b/include/lustrec_math.smt2
@@ -23,3 +23,4 @@
 (declare-rel exp ( Real Real) )
 (declare-rel log ( Real Real) )
 (declare-rel log10 ( Real Real) )
+(declare-rel tanh ( Real Real) )
\ No newline at end of file