Commit f2f79670 authored by MARCHE Claude's avatar MARCHE Claude

starting a regression test suite for counterexamples

parent c41a01ed
#!/bin/sh
case "$1" in
"-update-oracle")
updateoracle=true;;
"")
updateoracle=false;;
*)
echo "$0: Unknown option '$1'"
exit 2
esac
run_cvc4_15 () {
echo -n " $1... "
why3prove -P "CVC4,1.5-prerelease" --get-ce $1 > $1.out
if cmp $1.oracle $1.out > /dev/null 2>&1 ; then
echo "ok"
else
if $updateoracle; then
echo "Updating oracle for $1"
mv $1.out $1.oracle
else
echo "FAILED!"
echo "diff is the following:"
diff $1.oracle $1.out
fi
fi
}
for f in bench/ce/*.mlw; do
run_cvc4_15 $f
done
\ No newline at end of file
theory T
use import int.Int
goal g0 : forall x "model":int. ("model" x >= 42) -> ("model" x + 3 <= 50)
constant g : int
goal g1 : forall x "model":int. ("model" g >= x)
goal g2 : forall x1 "model" "model_trace:X" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
("model" "model_trace: X1 + 1 = 2" x1 + 1 = 2) ->
("model" x2 + 1 = 2) ->
("model" x3 + 1 = 2) ->
("model" x4 + 1 = 2) ->
("model" x5 + 1 = 2) ->
("model" x6 + 1 = 2) ->
("model" x7 + 1 = 2) ->
("model" x8 + 1 = 2) ->
("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
bench/ce/logic.mlw T g0 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 6:
x = {"type":"Integer",
"val":"48"}
bench/ce/logic.mlw T g1 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 10:
x = {"type":"Integer",
"val":"0"}
bench/ce/logic.mlw T g2 : Invalid (0.00s)
Counter-example model:File bench/ce/logic.mlw:
Line 12:
X = {"type":"Integer", "val":"1"}
x2 = {"type":"Integer",
"val":"1"}
x3 = {"type":"Integer", "val":"1"}
x4 = {"type":"Integer",
"val":"1"}
x5 = {"type":"Integer", "val":"1"}
x6 = {"type":"Integer",
"val":"1"}
x7 = {"type":"Integer", "val":"1"}
x8 = {"type":"Integer",
"val":"1"}
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