1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
new file mode 100644
index 000000000..dd9cb6886
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
+    or
+    (= n1 n 0)
+    (= n2 n 0)
+    (
+        and
+        (> n1 0)
+        (> n2 0)
+        (>= n 0)
+        (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0))))
+        (int-and (div n 2) (div n1 2) (div n2 2))
+    )
+))
+(check-sat)