test/regress/regress0/define-fun-model.smt2

   1 ; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/'
   2 ; EXPECT: sat
   3 ; EXPECT: (((f 4) 7))
   4 ; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7)))
   5 ; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7)))
   6 (set-logic UFLIA)
   7 (set-option :produce-models true)
   8 (define-fun f ((x Int)) Int 7)
   9 (declare-fun g (Int) Int)
  10
  11 (assert (= (g 5) (f 5)))
  12
  13 (check-sat)
  14 (get-value ((f 4)))
  15 (get-value (g))
  16 (get-value (f))