; File auto-generated by gentests.ml

; Auto-generated part begin
; Test for builtin-sort.smt2
; Incremental test

(rule
   (target  builtin-sort.incremental)
   (deps    (:input builtin-sort.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-sort.expected builtin-sort.incremental)))

; Full mode test

(rule
   (target  builtin-sort.full)
   (deps    (:input builtin-sort.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-sort.expected builtin-sort.full)))


; Test for builtin-term-const.smt2
; Incremental test

(rule
   (target  builtin-term-const.incremental)
   (deps    (:input builtin-term-const.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-term-const.expected builtin-term-const.incremental)))

; Full mode test

(rule
   (target  builtin-term-const.full)
   (deps    (:input builtin-term-const.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-term-const.expected builtin-term-const.full)))


; Test for builtin-term-var.smt2
; Incremental test

(rule
   (target  builtin-term-var.incremental)
   (deps    (:input builtin-term-var.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-term-var.expected builtin-term-var.incremental)))

; Full mode test

(rule
   (target  builtin-term-var.full)
   (deps    (:input builtin-term-var.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff builtin-term-var.expected builtin-term-var.full)))


; Test for def_fun_param.smt2
; Incremental test

(rule
   (target  def_fun_param.incremental)
   (deps    (:input def_fun_param.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_param.expected def_fun_param.incremental)))

; Full mode test

(rule
   (target  def_fun_param.full)
   (deps    (:input def_fun_param.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_param.expected def_fun_param.full)))


; Test for def_fun_param2.smt2
; Incremental test

(rule
   (target  def_fun_param2.incremental)
   (deps    (:input def_fun_param2.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_param2.expected def_fun_param2.incremental)))

; Full mode test

(rule
   (target  def_fun_param2.full)
   (deps    (:input def_fun_param2.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_param2.expected def_fun_param2.full)))


; Test for def_fun_rec_param.smt2
; Incremental test

(rule
   (target  def_fun_rec_param.incremental)
   (deps    (:input def_fun_rec_param.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_rec_param.expected def_fun_rec_param.incremental)))

; Full mode test

(rule
   (target  def_fun_rec_param.full)
   (deps    (:input def_fun_rec_param.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff def_fun_rec_param.expected def_fun_rec_param.full)))


; Test for redefinition.smt2
; Incremental test

(rule
   (target  redefinition.incremental)
   (deps    (:input redefinition.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff redefinition.expected redefinition.incremental)))

; Full mode test

(rule
   (target  redefinition.full)
   (deps    (:input redefinition.smt2))
   (package dolmen_bin)
   (action (chdir %{workspace_root}
            (with-outputs-to %{target}
             (with-accepted-exit-codes (or 0 (not 0))
              (run dolmen --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
(rule
  (alias runtest)
  (package dolmen_bin)
  (action (diff redefinition.expected redefinition.full)))


; Auto-generated part end