From a877ccdba81a0daafd08581bde264d2df6bac49b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1=C5=A1=20Dac=C3=ADk?= Date: Thu, 16 Jan 2025 19:01:17 +0100 Subject: [PATCH] [Test] Add test for input dump --- tests/API_tests.ml | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/tests/API_tests.ml b/tests/API_tests.ml index 397283f..ffe7a25 100644 --- a/tests/API_tests.ml +++ b/tests/API_tests.ml @@ -18,10 +18,21 @@ let check_sat_test2 () = in assert (not @@ Solver.check_sat solver phi) + +let debug_input () = + let dirname = Format.asprintf "%s/_astral_test" (Filename.get_temp_dir_name ()) in + let solver = Solver.init ~dump_queries:(`Full dirname) () in + let phi = SL.emp in + let _ = Solver.check_sat solver phi in + assert (Sys.file_exists @@ dirname ^ "/query_0001/input.smt2") + let () = run "API" [ + "debug", [ + test_case "input" `Quick debug_input; + ]; "check_sat", [ test_case "sat" `Quick check_sat_test1; test_case "unsat" `Quick check_sat_test2; - ]] - + ] + ]