From 71db47f9ac23f0b7d7ffaac2aea0fd531f1b07a7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 30 Oct 2019 15:03:24 -0500 Subject: [PATCH] test: more CC tests --- src/mini-cc/tests/tests.ml | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/src/mini-cc/tests/tests.ml b/src/mini-cc/tests/tests.ml index a0fe63c4..1b6d72fa 100644 --- a/src/mini-cc/tests/tests.ml +++ b/src/mini-cc/tests/tests.ml @@ -80,5 +80,28 @@ let () = mk_test "test_trans" @@ fun () -> A.(check bool) "is-unsat" (CC.check_sat cc) false; () +let () = mk_test "test_true" @@ fun () -> + let module S = Setup() in + let cc = CC.create S.tst in + CC.add_lit cc S.true_ true; + A.(check bool) "is-sat" (CC.check_sat cc) true; + CC.add_lit cc S.false_ true; + A.(check bool) "is-unsat" (CC.check_sat cc) false; + () + +let () = mk_test "test_false" @@ fun () -> + let module S = Setup() in + let cc = CC.create S.tst in + CC.add_lit cc S.false_ true; + A.(check bool) "is-unsat" (CC.check_sat cc) false; + () + +let () = mk_test "test_not_false" @@ fun () -> + let module S = Setup() in + let cc = CC.create S.tst in + CC.add_lit cc S.(not_ false_) true; + A.(check bool) "is-sat" (CC.check_sat cc) true; + () + (* run alcotest *) let () = Alcotest.run "mini-cc-tests" ["mini-cc", List.rev !l]