test for uninterpreted functions

This adds a test for an uninterpreted function, added using declare-fun.

Author: kroening

regression/smt2_solver/uninterpreted-functions/uf1.desc

@@ -0,0 +1,7 @@
+CORE
+uf1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/uninterpreted-functions/uf1.smt2

@@ -0,0 +1,11 @@
+(set-logic QF_UFBV)
+
+(declare-fun myfun ((_ BitVec 32)) (_ BitVec 32))
+
+(assert (= (myfun (_ bv10 32)) (_ bv20 32)))
+
+(declare-const x (_ BitVec 32))
+(assert (= x (_ bv10 32)))
+(assert (= (myfun x) (_ bv30 32)))
+
+(check-sat)