1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/bug782.smt2 b/test/regress/regress0/fmf/bug782.smt2
new file mode 100644
index 000000000..603c783d3
--- /dev/null
+++ b/test/regress/regress0/fmf/bug782.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(define-fun $$Bool.isTrue$$ ((b Bool)) Bool b)
+(define-fun $$Bool.isFalse$$ ((b Bool)) Bool (not b))
+
+(define-funs-rec
+  (
+    (f123454321$multipleArgsFunction((x$$645421 Bool) (y$$645422 Bool)) Bool)
+    (f12345678$myConst() Int)
+  )
+  (
+    (= x$$645421 y$$645422)
+    3
+  )
+)
+
+(declare-fun i1000$$1000() Bool)
+(declare-fun i1001$$1001() Bool)
+(declare-fun i1002$$1002() Int)
+(assert (f123454321$multipleArgsFunction i1000$$1000 i1001$$1001))
+(assert (= i1002$$1002 f12345678$myConst))
+(check-sat)