diff --git a/pysmt/smtlib/parser/parser.py b/pysmt/smtlib/parser/parser.py
index bf093d6..abbca6e 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -876,7 +876,6 @@ class SmtLibParser(object):
                                        "command." % command,
                                        tokens.pos_info)
             res.append(current)
-
         for _ in xrange(min_size, max_size + 1):
             current = tokens.consume()
             if current == ")":
@@ -1170,16 +1169,18 @@ class SmtLibParser(object):
         var = self.parse_atom(tokens, current)
         namedparams = self.parse_named_params(tokens, current)
         rtype = self.parse_type(tokens, current)
-
+        bindings = []
         for (x,t) in namedparams:
-            v = self._get_var(x, t)
+            v = self.env.formula_manager.FreshSymbol(typename=t,
+                                                        template="__"+x+"%d")
             self.cache.bind(x, v)
-            formal.append(v)
+            formal.append(v) #remember the variable
+            bindings.append(x) #remember the name
         # Parse expression using also parameters
         ebody = self.get_expression(tokens)
-        # Discard parameters
-        for x in formal:
-            self.cache.unbind(x.symbol_name())
+        #Discard parameters
+        for x in bindings:
+            self.cache.unbind(x)
         # Finish Parsing
         self.consume_closing(tokens, current)
         self.cache.define(var, formal, ebody)

PysmtTypeError when reusing symbols in SMT-LIB define-fun
In the following SMT-LIB definitions, I am using `n` as an Int parameter for `f` and as a Real parameter for `g`:
```
(define-fun f ((n Int)) Int n)
(define-fun g ((n Real)) Real n)
```
This yields PysmtTypeError, saying: `Trying to redefine symbol 'n' with a new type. Previous type was 'Int' new type is 'Real'`.

This should not happen - according to the [standard](http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf) (p. 62), `(define-fun f ((n Int)) n)` is equivalent to:
```
(declare-fun f ((n Int) n)
(assert (forall ((n Int)) (= (f n) n)))
```
And so there shouldn't be a problem re-using n.

To reproduce:
`python tmp.py` for `tmp.py` with the following content:

```
from pysmt.smtlib.parser import SmtLibParser
import os

def main():
    smtlib_script = '\n'.join(['(define-fun f ((n Int)) Int n)', '(define-fun g ((n Real)) Real n)'])
    tmp_file_name = "tmp.smt2"
    tmp_file = open(tmp_file_name, 'w')
    tmp_file.write(smtlib_script)
    tmp_file.close()
    parser = SmtLibParser()
    script = parser.get_script_fname(tmp_file_name)
    os.remove(tmp_file_name)

if __name__ == "__main__":
    main()
```
diff --git a/pysmt/test/smtlib/test_smtlibscript.py b/pysmt/test/smtlib/test_smtlibscript.py
index 2f97538..bcb66cf 100644
--- a/pysmt/test/smtlib/test_smtlibscript.py
+++ b/pysmt/test/smtlib/test_smtlibscript.py
@@ -16,7 +16,6 @@
 #   limitations under the License.
 #
 from six.moves import cStringIO
-
 import pysmt.smtlib.commands as smtcmd
 from pysmt.shortcuts import And, Or, Symbol, GT, Real, Not
 from pysmt.typing import REAL
@@ -122,6 +121,19 @@ class TestSmtLibScript(TestCase):
             f = get_formula_strict(stream_in)
 
 
+    #n is defined once as an Int and once as a Real
+    def test_define_funs_same_args(self):
+        smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(define-fun f ((n Real)) Real n)'])
+        stream = cStringIO(smtlib_script)
+        parser = SmtLibParser()
+        script = parser.get_script(stream)
+
+    def test_define_funs_arg_and_fun(self):
+        smtlib_script = "\n".join(['(define-fun f ((n Int)) Int n)', '(declare-fun n () Real)'])
+        stream = cStringIO(smtlib_script)
+        parser = SmtLibParser()
+        script = parser.get_script(stream)
+
     def test_evaluate_command(self):
         class SmtLibIgnore(SmtLibIgnoreMixin):
             pass
@@ -207,6 +219,12 @@ DEMO_SMTSCRIPT = [ "(declare-fun a () Bool)",
                    "(define-sort G (H) (F Int H))",
                    "(define-fun f ((a Bool)) B a)",
                    "(define-fun g ((a Bool)) B (f a))",
+                   "(define-fun h ((a Int)) Int a)",
+                   "(declare-const x Bool)",
+                   "(declare-const y Int)",
+                   "(assert (= (h y) y))",
+                   "(assert (= (f x) x))",
+                   "(check-sat)",
                    "(define-fun-rec f ((a A)) B a)",
                    "(define-fun-rec g ((a A)) B (g a))",
                    """(define-funs-rec ((h ((a A)) B) (i ((a A)) B) )
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index a33c576..da2f2b6 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -393,7 +393,7 @@ class TestRegressions(TestCase):
         s = parser.get_script(buffer_)
         for c in s:
             res = c.serialize_to_string(daggify=False)
-        self.assertEqual(res, smtlib_input)
+        self.assertEqual(res.replace('__x0', 'x'), smtlib_input)
 
     @skipIfSolverNotAvailable("z3")
     def test_z3_nary_back(self):

pip install -e .[dev]
parse_log_pytest
requirements.txt
pytest
apt-get update apt-get install -y gcc
3.9
dev-requirements.txt
pytest --no-header -rA --tb=line --color=no -p no:cacheprovider -W ignore::DeprecationWarning
exceptiongroup==1.2.2
iniconfig==2.1.0
nose==1.3.7
packaging==24.2
pluggy==1.5.0
-e git+https://github.com/pysmt/pysmt.git@b0324e68bee72c862db9620206a34f2e20c38160#egg=PySMT
pytest==8.3.5
six==1.17.0
tomli==2.2.1

name: pysmt
channels:
  - defaults
  - https://repo.anaconda.com/pkgs/main
  - https://repo.anaconda.com/pkgs/r
  - conda-forge
dependencies:
  - _libgcc_mutex=0.1=main
  - _openmp_mutex=5.1=1_gnu
  - ca-certificates=2025.2.25=h06a4308_0
  - ld_impl_linux-64=2.40=h12ee557_0
  - libffi=3.4.4=h6a678d5_1
  - libgcc-ng=11.2.0=h1234567_1
  - libgomp=11.2.0=h1234567_1
  - libstdcxx-ng=11.2.0=h1234567_1
  - ncurses=6.4=h6a678d5_0
  - openssl=3.0.16=h5eee18b_0
  - pip=25.0=py39h06a4308_0
  - python=3.9.21=he870216_1
  - readline=8.2=h5eee18b_0
  - setuptools=75.8.0=py39h06a4308_0
  - sqlite=3.45.3=h5eee18b_0
  - tk=8.6.14=h39e8969_0
  - tzdata=2025a=h04d1e81_0
  - wheel=0.45.1=py39h06a4308_0
  - xz=5.6.4=h5eee18b_1
  - zlib=1.2.13=h5eee18b_1
  - pip:
      - exceptiongroup==1.2.2
      - iniconfig==2.1.0
      - nose==1.3.7
      - packaging==24.2
      - pluggy==1.5.0
      - pytest==8.3.5
      - six==1.17.0
      - tomli==2.2.1
prefix: /opt/conda/envs/pysmt

pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_all_parsing
pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_define_funs_arg_and_fun pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_define_funs_same_args pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_get_strict_formula pysmt/test/test_regressions.py::TestRegressions::test_parse_bvconst_width pysmt/test/test_regressions.py::TestRegressions::test_parse_bvx_var pysmt/test/test_regressions.py::TestRegressions::test_parse_declare_const pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun pysmt/test/test_regressions.py::TestRegressions::test_parse_define_fun_bind pysmt/test/test_regressions.py::TestRegressions::test_smtlib_define_fun_serialization pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_parsing
pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_basic_operations pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_evaluate_command pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_from_formula pysmt/test/smtlib/test_smtlibscript.py::TestSmtLibScript::test_smtlibignore_mixin pysmt/test/test_regressions.py::TestRegressions::test_array_initialization_printing pysmt/test/test_regressions.py::TestRegressions::test_cnf_as_set pysmt/test/test_regressions.py::TestRegressions::test_dependencies_not_includes_toreal pysmt/test/test_regressions.py::TestRegressions::test_determinism pysmt/test/test_regressions.py::TestRegressions::test_empty_string_symbol pysmt/test/test_regressions.py::TestRegressions::test_equality_typing pysmt/test/test_regressions.py::TestRegressions::test_exactly_one_unpacking pysmt/test/test_regressions.py::TestRegressions::test_exactlyone_w_generator pysmt/test/test_regressions.py::TestRegressions::test_git_version pysmt/test/test_regressions.py::TestRegressions::test_infix_notation_wrong_le pysmt/test/test_regressions.py::TestRegressions::test_is_one pysmt/test/test_regressions.py::TestRegressions::test_multiple_declaration_w_same_functiontype pysmt/test/test_regressions.py::TestRegressions::test_multiple_exit pysmt/test/test_regressions.py::TestRegressions::test_parse_exception pysmt/test/test_regressions.py::TestRegressions::test_qf_bool_smt2 pysmt/test/test_regressions.py::TestRegressions::test_simplify_times pysmt/test/test_regressions.py::TestRegressions::test_simplifying_int_plus_changes_type_of_expression pysmt/test/test_regressions.py::TestRegressions::test_smtlib_info_quoting pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_hr_printer pysmt/test/test_regressions.py::TestRegressions::test_string_constant_quote_escaping_smtlib_printer pysmt/test/test_regressions.py::TestRegressions::test_substitute_memoization pysmt/test/test_regressions.py::TestRegressions::test_substitute_to_real
pysmt/smtlib/parser/parser.py
pysmt/smtlib/parser/parser.py