1 ; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/'
4 ; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7)))
5 ; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7)))
7 (set-option :produce-models true)
8 (define-fun f ((x Int)) Int 7)
9 (declare-fun g (Int) Int)
11 (assert (= (g 5) (f 5)))