blob: 459ca8fd66f98fbf1190b276b451ba32482e6752 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Smtcoq_extr
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat1.cnf\" \"../../unit-tests/sat1.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat1.cnf" "../../unit-tests/sat1.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat2.cnf\" \"../../unit-tests/sat2.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat2.cnf" "../../unit-tests/sat2.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat3.cnf\" \"../../unit-tests/sat3.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat3.cnf" "../../unit-tests/sat3.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat5.cnf\" \"../../unit-tests/sat5.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat5.cnf" "../../unit-tests/sat5.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat6.cnf\" \"../../unit-tests/sat6.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat6.cnf" "../../unit-tests/sat6.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/sat7.cnf\" \"../../unit-tests/sat7.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/sat7.cnf" "../../unit-tests/sat7.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/hole4.cnf\" \"../../unit-tests/hole4.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/hole4.cnf" "../../unit-tests/hole4.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/cmu-bmc-barrel6.cnf\" \"../../unit-tests/cmu-bmc-barrel6.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/cmu-bmc-barrel6.cnf" "../../unit-tests/cmu-bmc-barrel6.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"../../unit-tests/velev-sss-1.0-05.cnf\" \"../../unit-tests/velev-sss-1.0-05.zlog\" = %b\n" (Zchaff_checker.checker "../../unit-tests/velev-sss-1.0-05.cnf" "../../unit-tests/velev-sss-1.0-05.zlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat0.smt2\" \"../../unit-tests/sat0.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat0.smt2" "../../unit-tests/sat0.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat1.smt2\" \"../../unit-tests/sat1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat1.smt2" "../../unit-tests/sat1.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat2.smt2\" \"../../unit-tests/sat2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat2.smt2" "../../unit-tests/sat2.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat3.smt2\" \"../../unit-tests/sat3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat3.smt2" "../../unit-tests/sat3.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat4.smt2\" \"../../unit-tests/sat4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat4.smt2" "../../unit-tests/sat4.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat5.smt2\" \"../../unit-tests/sat5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat5.smt2" "../../unit-tests/sat5.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat6.smt2\" \"../../unit-tests/sat6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat6.smt2" "../../unit-tests/sat6.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat7.smt2\" \"../../unit-tests/sat7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat7.smt2" "../../unit-tests/sat7.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat8.smt2\" \"../../unit-tests/sat8.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat8.smt2" "../../unit-tests/sat8.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat9.smt2\" \"../../unit-tests/sat9.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat9.smt2" "../../unit-tests/sat9.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat11.smt2\" \"../../unit-tests/sat11.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat11.smt2" "../../unit-tests/sat11.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat12.smt2\" \"../../unit-tests/sat12.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat12.smt2" "../../unit-tests/sat12.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat13.smt2\" \"../../unit-tests/sat13.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat13.smt2" "../../unit-tests/sat13.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/sat14.smt2\" \"../../unit-tests/sat14.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/sat14.smt2" "../../unit-tests/sat14.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/hole4.smt2\" \"../../unit-tests/hole4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/hole4.smt2" "../../unit-tests/hole4.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf1.smt2\" \"../../unit-tests/uf1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf1.smt2" "../../unit-tests/uf1.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf2.smt2\" \"../../unit-tests/uf2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf2.smt2" "../../unit-tests/uf2.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf3.smt2\" \"../../unit-tests/uf3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf3.smt2" "../../unit-tests/uf3.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf4.smt2\" \"../../unit-tests/uf4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf4.smt2" "../../unit-tests/uf4.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf5.smt2\" \"../../unit-tests/uf5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf5.smt2" "../../unit-tests/uf5.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf6.smt2\" \"../../unit-tests/uf6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf6.smt2" "../../unit-tests/uf6.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/uf7.smt2\" \"../../unit-tests/uf7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/uf7.smt2" "../../unit-tests/uf7.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia1.smt2\" \"../../unit-tests/lia1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia1.smt2" "../../unit-tests/lia1.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia2.smt2\" \"../../unit-tests/lia2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia2.smt2" "../../unit-tests/lia2.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia3.smt2\" \"../../unit-tests/lia3.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia3.smt2" "../../unit-tests/lia3.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia4.smt2\" \"../../unit-tests/lia4.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia4.smt2" "../../unit-tests/lia4.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia5.smt2\" \"../../unit-tests/lia5.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia5.smt2" "../../unit-tests/lia5.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia6.smt2\" \"../../unit-tests/lia6.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia6.smt2" "../../unit-tests/lia6.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/lia7.smt2\" \"../../unit-tests/lia7.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/lia7.smt2" "../../unit-tests/lia7.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/let1.smt2\" \"../../unit-tests/let1.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/let1.smt2" "../../unit-tests/let1.vtlog")
let _ = Printf.printf "Verit_checker.checker \"../../unit-tests/let2.smt2\" \"../../unit-tests/let2.vtlog\" = %b\n" (Verit_checker.checker "../../unit-tests/let2.smt2" "../../unit-tests/let2.vtlog")
|
