We got back all the tests of Popop

   except the one about efficiency with learning

src_colibri2/popop_lib/debug.ml

@@ -108,6 +108,7 @@ let real_dprintf ?nobox s =
   Format.kfprintf
     (fun fmt -> if box then begin
          Format.pp_close_box fmt ();
+         Format.pp_print_flush fmt ();
        end
     )
     !formatter s

src_colibri2/tests/generate_tests/generate_dune_tests.ml

@@ -3,7 +3,7 @@ let result = Sys.argv.(2)
 
 let print_test cout file =
   Printf.fprintf cout
-    "(rule (action (with-stdout-to %s.res (run colibri2 --max-step 1000 %s))))\n"
+    "(rule (action (with-stdout-to %s.res (run %%{bin:colibri2} --max-step 1000 %%{dep:%s}))))\n"
     file file;
   Printf.fprintf cout
     "(rule (alias runtest) (action (diff oracle %s.res)))\n"

src_colibri2/tests/solve/dimacs/sat/dune.inc

 (rule (action (with-stdout-to oracle (echo "sat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold2.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold2.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold2.cnf.res)))
-(rule (action (with-stdout-to assertion_fail.cnf.res (run colibri2 --max-step 1000 assertion_fail.cnf))))
+(rule (action (with-stdout-to assertion_fail.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:assertion_fail.cnf}))))
 (rule (alias runtest) (action (diff oracle assertion_fail.cnf.res)))
-(rule (action (with-stdout-to fuzzing1.cnf.res (run colibri2 --max-step 1000 fuzzing1.cnf))))
+(rule (action (with-stdout-to fuzzing1.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:fuzzing1.cnf}))))
 (rule (alias runtest) (action (diff oracle fuzzing1.cnf.res)))
-(rule (action (with-stdout-to fuzzing2.cnf.res (run colibri2 --max-step 1000 fuzzing2.cnf))))
+(rule (action (with-stdout-to fuzzing2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:fuzzing2.cnf}))))
 (rule (alias runtest) (action (diff oracle fuzzing2.cnf.res)))
-(rule (action (with-stdout-to par8-1-c.cnf.res (run colibri2 --max-step 1000 par8-1-c.cnf))))
+(rule (action (with-stdout-to par8-1-c.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:par8-1-c.cnf}))))
 (rule (alias runtest) (action (diff oracle par8-1-c.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-2.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-3.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-4.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))
-(rule (action (with-stdout-to quinn.cnf.res (run colibri2 --max-step 1000 quinn.cnf))))
+(rule (action (with-stdout-to quinn.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:quinn.cnf}))))
 (rule (alias runtest) (action (diff oracle quinn.cnf.res)))
-(rule (action (with-stdout-to simple_v3_c2.cnf.res (run colibri2 --max-step 1000 simple_v3_c2.cnf))))
+(rule (action (with-stdout-to simple_v3_c2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:simple_v3_c2.cnf}))))
 (rule (alias runtest) (action (diff oracle simple_v3_c2.cnf.res)))

src_colibri2/tests/solve/dimacs/unsat/dune.inc

 (rule (action (with-stdout-to oracle (echo "unsat\n"))))
-(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run colibri2 --max-step 1000 anomaly_agetooold.cnf))))
+(rule (action (with-stdout-to anomaly_agetooold.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:anomaly_agetooold.cnf}))))
 (rule (alias runtest) (action (diff oracle anomaly_agetooold.cnf.res)))
-(rule (action (with-stdout-to modus_ponens.cnf.res (run colibri2 --max-step 1000 modus_ponens.cnf))))
+(rule (action (with-stdout-to modus_ponens.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:modus_ponens.cnf}))))
 (rule (alias runtest) (action (diff oracle modus_ponens.cnf.res)))
-(rule (action (with-stdout-to pigeon-1.cnf.res (run colibri2 --max-step 1000 pigeon-1.cnf))))
+(rule (action (with-stdout-to pigeon-1.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-1.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-1.cnf.res)))
-(rule (action (with-stdout-to pigeon-2.cnf.res (run colibri2 --max-step 1000 pigeon-2.cnf))))
+(rule (action (with-stdout-to pigeon-2.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-2.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-2.cnf.res)))
-(rule (action (with-stdout-to pigeon-3.cnf.res (run colibri2 --max-step 1000 pigeon-3.cnf))))
+(rule (action (with-stdout-to pigeon-3.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-3.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-3.cnf.res)))
-(rule (action (with-stdout-to pigeon-4.cnf.res (run colibri2 --max-step 1000 pigeon-4.cnf))))
+(rule (action (with-stdout-to pigeon-4.cnf.res (run %{bin:colibri2} --max-step 1000 %{dep:pigeon-4.cnf}))))
 (rule (alias runtest) (action (diff oracle pigeon-4.cnf.res)))

tests/smtlib2/lra/sat/arith_mult_explication.smt2 → src_colibri2/tests/solve/smt_lra/sat/arith_mult_explication.smt2

-(set-logic QF_LRA)
+(set-logic ALL)
 (declare-fun v0 () Real)
 (declare-fun b () Bool)
 (assert