diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml index 0fdc0fbb1594b836848c50b46d51a3df0075de48..0295d640b6029ee4c9cefb487a74701f9efad8a5 100644 --- a/src/testsuite/cool-testsuite.ml +++ b/src/testsuite/cool-testsuite.ml @@ -31,21 +31,21 @@ let k_testcases: satCheck list = ; c Unsat "False" ; c ParseError "{Fsdf" (*; c ParseError "Fsdf}" *) - ; c Unsat "<R> True & [R] False" - ; c Unsat "C |- <R> ~C" - ; c Sat "C |- [R] ~C" - ; c Unsat "<R> ((<R> C) & (<S> False))" - ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))" - ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))" - ; c Sat "<R> a & <R> B |- [R] C" - ; c Unsat "<R> a & <R> B |- [R] (~a & ~B)" - ; c Unsat "<R> a & <R> B |- [R] ~B" - ; c Sat "<R> a & <R> ~a |- [R] B" - ; c Unsat "<R> a & <R> ~a & (B => [R] ~a) |- [R] B" - ; c Sat "<R> a & <R> ~a & (B => [R] ~a) & (C => ~D) & (D => ~e) & <R> C & <R> D & <R> e |- True" - ; c Unsat "<R> D & <R> e & ((<R> D & <R> e) => [R] e) & ~(D & e) |- True" - ; c Sat "(<R> D | <R> e) & ((<R> D & <R> e) => [R] e) & ~(D & e) |- True" - ; c Sat "<R> D & <R> e & ((<R> D & <R> e) => [R] e) & (D & e => <R> ~(D&e)) |- True" + ; c Unsat "<r> True & [r] False" + ; c Unsat "c |- <r> ~c" + ; c Sat "c |- [r] ~c" + ; c Unsat "<r> ((<r> c) & (<s> False))" + ; c Unsat "<x> (<s> False) | <r> ((<r> c) & (<s> False))" + ; c Unsat "<x> (<s> False) | <r> ((<r> c) & (<s> False))" + ; c Sat "<r> a & <r> b |- [r] c" + ; c Unsat "<r> a & <r> b |- [r] (~a & ~b)" + ; c Unsat "<r> a & <r> b |- [r] ~b" + ; c Sat "<r> a & <r> ~a |- [r] b" + ; c Unsat "<r> a & <r> ~a & (b => [r] ~a) |- [r] b" + ; c Sat "<r> a & <r> ~a & (b => [r] ~a) & (c => ~d) & (d => ~e) & <r> c & <r> d & <r> e |- True" + ; c Unsat "<r> d & <r> e & ((<r> d & <r> e) => [r] e) & ~(d & e) |- True" + ; c Sat "(<r> d | <r> e) & ((<r> d & <r> e) => [r] e) & ~(d & e) |- True" + ; c Sat "<r> d & <r> e & ((<r> d & <r> e) => [r] e) & (d & e => <r> ~(d&e)) |- True" ]