Also test parallel checker in integration tests

carcara/tests/test_example_files.rs

@@ -4,6 +4,34 @@ use std::{
     path::{Path, PathBuf},
 };
 
+fn run_parallel_checker_test(
+    problem_path: &Path,
+    proof_path: &Path,
+    num_threads: usize,
+) -> CarcaraResult<()> {
+    use checker::Config;
+    use std::sync::Arc;
+
+    let (prelude, proof, pool) = parser::parse_instance(
+        io::BufReader::new(fs::File::open(problem_path)?),
+        io::BufReader::new(fs::File::open(proof_path)?),
+        false,
+        false,
+        false,
+    )?;
+
+    let (scheduler, schedule_context_usage) = checker::Scheduler::new(num_threads, &proof);
+    let mut checker = checker::ParallelProofChecker::new(
+        Arc::new(pool),
+        Config::new(),
+        &prelude,
+        &schedule_context_usage,
+        128 * 1024 * 1024,
+    );
+    checker.check(&proof, &scheduler)?;
+    Ok(())
+}
+
 fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {
     use checker::Config;
 
@@ -35,6 +63,11 @@ fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {
         "elaboration was not idempotent!"
     );
 
+    // We also test the parallel checker, with different values for the number of threads
+    run_parallel_checker_test(problem_path, proof_path, 1)?;
+    run_parallel_checker_test(problem_path, proof_path, 4)?;
+    run_parallel_checker_test(problem_path, proof_path, 16)?;
+
     Ok(())
 }