add test for SMT-LIB2 parameter scopes

SMT-LIB2 function definitions have scopes for the identifiers of the parameters.

This was raised in #5143.

Author: kroening

regression/smt2_solver/function-applications/function-scoping1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+function-scoping1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--
+^\(error

regression/smt2_solver/function-applications/function-scoping1.smt2

@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+
+; the function parameters are in a separate scope
+
+(define-fun min ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8)
+    (ite (bvule a b) a b))
+
+(declare-const a (_ BitVec 32))
+
+(assert (not (= a a)))
+
+(check-sat)