1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2
new file mode 100644
index 000000000..c6ca206fc
--- /dev/null
+++ b/test/regress/regress0/define-fun-model.smt2
@@ -0,0 +1,16 @@
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/'
+; EXPECT: sat
+; EXPECT: (((f 4) 7))
+; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7)))
+; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7)))
+(set-logic UFLIA)
+(set-option :produce-models true)
+(define-fun f ((x Int)) Int 7)
+(declare-fun g (Int) Int)
+
+(assert (= (g 5) (f 5)))
+
+(check-sat)
+(get-value ((f 4)))
+(get-value (g))
+(get-value (f))