; File auto-generated by gentests.ml

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

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

; Full mode test

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


; Test for array_const.smt2
; Incremental test

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

; Full mode test

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


; Test for comparison_abstract.smt2
; Incremental test

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

; Full mode test

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


; Auto-generated part end