; File auto-generated by gentests.ml

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

(rule
   (target  smtlib_error.incremental)
   (deps    (:input smtlib_error.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 smtlib_error.expected smtlib_error.incremental)))

; Full mode test

(rule
   (target  smtlib_error.full)
   (deps    (:input smtlib_error.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 smtlib_error.expected smtlib_error.full)))


; Test for smtlib_ok.smt2
; Incremental test

(rule
   (target  smtlib_ok.incremental)
   (deps    (:input smtlib_ok.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 smtlib_ok.expected smtlib_ok.incremental)))

; Full mode test

(rule
   (target  smtlib_ok.full)
   (deps    (:input smtlib_ok.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 smtlib_ok.expected smtlib_ok.full)))


; Test for smtlib_warn.smt2
; Incremental test

(rule
   (target  smtlib_warn.incremental)
   (deps    (:input smtlib_warn.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 smtlib_warn.expected smtlib_warn.incremental)))

; Full mode test

(rule
   (target  smtlib_warn.full)
   (deps    (:input smtlib_warn.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 smtlib_warn.expected smtlib_warn.full)))


; Auto-generated part end