diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-24 09:49:47 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-24 09:49:47 +0200 |
| commit | 5ebe1f1c3684609dc0c2f360cf4d86486795ab54 (patch) | |
| tree | 2c9b42c9f116f3d75c550c3a3bc627d30393d66a /unit-tests | |
| parent | ca7adf2ee2106667f6de91b3a1ee755f69087e54 (diff) | |
| download | smtcoq-5ebe1f1c3684609dc0c2f360cf4d86486795ab54.tar.gz smtcoq-5ebe1f1c3684609dc0c2f360cf4d86486795ab54.zip | |
The simplest test for SMT
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit.v | 13 | ||||
| -rw-r--r-- | unit-tests/sat0.smt2 | 4 |
2 files changed, 17 insertions, 0 deletions
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 837e3e9..2be8752 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -6,6 +6,10 @@ Local Open Scope int63_scope. (* veriT vernacular commands *) +Section Checker_Sat0. + Verit_Checker "sat0.smt2" "sat0.vtlog". +End Checker_Sat0. + Section Checker_Sat1. Verit_Checker "sat1.smt2" "sat1.vtlog". End Checker_Sat1. @@ -129,6 +133,11 @@ End Checker_Let2. *) +Section Sat0. + Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog". + Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. +End Sat0. + Section Sat1. Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog". Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1. @@ -277,6 +286,10 @@ End Let2. *) +Section Theorem_Sat0. + Time Verit_Theorem theorem_sat1 "sat0.smt2" "sat0.vtlog". +End Theorem_Sat0. + Section Theorem_Sat1. Time Verit_Theorem theorem_sat1 "sat1.smt2" "sat1.vtlog". End Theorem_Sat1. diff --git a/unit-tests/sat0.smt2 b/unit-tests/sat0.smt2 new file mode 100644 index 0000000..ee93259 --- /dev/null +++ b/unit-tests/sat0.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_UF) +(assert false) +(check-sat) +(exit) |