alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

bitvect: Fix routines for 64-width vectors

Browse source 
* src/misc/bitvect.hh: Here.
* src/tgbatest/det.test, src/ltltest/ltlfilt.test: Add test cases.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-13 18:44:46 +01:00
parent be40885010
commit 7daea8d3cb
3 changed files with 53 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ltltest/ltlfilt.test
View file

@ -179,3 +179,9 @@ grep 'invalid' stderr
SPOT_STUTTER_CHECK=5 \
../../bin/ltlfilt --stutter-invariant -f '!{a:b*:c}'
# This one was incorrectly diagnosed as stutter invariant because of a
# bug in the bitvectors.
../../bin/ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
true