simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Added test for bug (conflict at level 0)

Browse source
This commit is contained in:
Guillaume Bury 2016-11-21 15:51:55 +01:00
parent 38972d7fc6
commit b88b906da9
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
tests/test_api.ml
View file

@ -144,6 +144,18 @@ module Test = struct
solve `Expect_unsat; solve `Expect_unsat;
] |> mk_test "test3" ] |> mk_test "test3"
(* Conflict at level 0 *)
let test4 =
[ assume [[-1; -2]];
solve `Expect_sat;
assume [[1]];
solve `Expect_sat;
assume [[2]];
solve ~assumptions:[3] `Expect_unsat;
solve ~assumptions:[] `Expect_unsat;
solve ~assumptions:[] `Expect_unsat;
] |> mk_test "conflict0"
(* just check that we do create new solvers *) (* just check that we do create new solvers *)
let test_clean = let test_clean =
[ solve `Expect_sat [ solve `Expect_sat
@ -153,6 +165,7 @@ module Test = struct
[ test1; [ test1;
test2; test2;
test3; test3;
test4;
test_clean; (* after test3 *) test_clean; (* after test3 *)
] ]
end end