Commit b5352205 authored by Thorsten Wißmann's avatar Thorsten Wißmann
Browse files

Only use addBSNoChk for simple bitsets

Insert a formula into a bitset without checking for a contradiction. The
former addBS performed a contradiction-check using MiscSolver.arrayNeg
which is a array of size 0 due to not being initialized.

For some reasons this bug only could be triggered when building with
oasis and not with the old Makefile, though arrayNeg being of size 0 in
both cases.

This fixes #12.
parent ed3a7d47
......@@ -79,7 +79,7 @@ let mkRule_MultiModalKD sort bs sl =
(* step 1: for each ∀R._ add R *)
let addRoleIfBox formula =
if lfGetType sort formula = AxF then
ignore (S.addBS roles (lfGetDest3 sort formula))
ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
else ()
in
bsetIter (addRoleIfBox) bs;
......@@ -274,7 +274,7 @@ let mkRule_GML sort bs sl =
let roles = S.makeBS () in
(* step 1: for each diamond/box add R *)
let addRole formula =
ignore (S.addBS roles (lfGetDest3 sort formula))
ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
in
bsetIter addRole boxes;
bsetIter addRole diamonds;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment