Skip to content
Snippets Groups Projects
Commit 66d3531d authored by Arthur Correnson's avatar Arthur Correnson
Browse files

Automatic tests in smt_fp

parent 84a95ff2
No related branches found
No related tags found
1 merge request!12Feature/fp check
Pipeline #35257 passed
(include dune.inc)
(rule
(alias runtest)
(deps
(glob_files *.cnf)
(glob_files *.smt2)
(glob_files *.psmt2))
(action
(with-stdout-to
dune.inc
(run %{exe:../../../generate_tests/generate_dune_tests.exe} . sat)))
(mode promote))
(rule (action (with-stdout-to oracle (echo "sat\n"))))
(rule (action (with-stdout-to recognize_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_float32.smt2}))))
(rule (alias runtest) (action (diff oracle recognize_float32.smt2.res)))
(rule (action (with-stdout-to recognize_float64.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_float64.smt2}))))
(rule (alias runtest) (action (diff oracle recognize_float64.smt2.res)))
(rule (action (with-stdout-to recognize_rounding_mode.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:recognize_rounding_mode.smt2}))))
(rule (alias runtest) (action (diff oracle recognize_rounding_mode.smt2.res)))
(rule (action (with-stdout-to simple_add_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_add_float32.smt2}))))
(rule (alias runtest) (action (diff oracle simple_add_float32.smt2.res)))
(rule (action (with-stdout-to simple_mul_float32.smt2.res (run %{bin:colibri2} --max-steps 3000 %{dep:simple_mul_float32.smt2}))))
(rule (alias runtest) (action (diff oracle simple_mul_float32.smt2.res)))
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment