From 5ebe1f1c3684609dc0c2f360cf4d86486795ab54 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Sun, 24 Apr 2016 09:49:47 +0200
Subject: The simplest test for SMT

---
 unit-tests/Tests_verit.v | 13 +++++++++++++
 unit-tests/sat0.smt2     |  4 ++++
 2 files changed, 17 insertions(+)
 create mode 100644 unit-tests/sat0.smt2

(limited to 'unit-tests')

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)
-- 
cgit