add tests for SMT-LIB2 function and let scopes

SMT-LIB2 function definitions have scopes for the identifiers of the
parameters.  The same holds for let expressions.

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)

regression/smt2_solver/let1/let-scoping1.desc

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

regression/smt2_solver/let1/let-scoping1.smt2

@@ -0,0 +1,12 @@
+(set-logic QF_BV)
+
+; the let parameters are in a separate scope
+
+; let hides the function 'x'
+(define-fun let1 () Bool (let ((a true)) a))
+
+(declare-const a (_ BitVec 32))
+
+(assert (not (= a a)))
+
+(check-sat)