make bench now checks invalid goals as well

parent 014b5455
......@@ -66,6 +66,20 @@ valid_goals () {
done
}
invalid_goals () {
for f in $1/*.mlw; do
echo -n " "$f"... "
if $pgm -t 3 -P alt-ergo $f | grep -q Valid; then
echo "invalid test $f failed!"
echo "$pgm -P alt-ergo $f"
$pgm -t 3 -P alt-ergo $f
exit 1
else
echo "ok"
fi
done
}
execute () {
echo -n "$1 $2... "
if $pgm $1 --exec $2 > /dev/null 2>&1; then
......@@ -119,6 +133,10 @@ list_stuff () {
fi
}
echo "=== Checking invalid goals ==="
invalid_goals bench/invalid
echo ""
echo "=== Checking theories ==="
goods theories
echo ""
......
module Arith
use import int.Int
goal G1: 0 = 1
use import int.ComputerDivision
goal G2: div 1 0 = div 2 0
end
module False
goal F: false
end
Markdown is supported
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