Repository: pysmt/pysmt

Issue:
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()
```

Discussion:

Patch:
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)


Test patch:
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):