Project

General

Profile

« Previous | Next » 

Revision f01a1af8

Added by Pierre-Loïc Garoche over 7 years ago

Update on the test script

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@265 041b043f-8d7c-46b2-b46e-ef0dd855326e

View differences:

test/test-compile.sh
116 116
    fi	
117 117
	# Cheching witness
118 118
    pushd $build > /dev/null
119
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus -verbose 0
119
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
120 120
    popd > /dev/null
121 121
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
122 122
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
126 126
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
127 127
	rinlining="UNKNOWN";
128 128
    else
129
	rinlining="INVALID"
130
	exit 1
129
	rinlining="INVALID/TIMEOUT"
131 130
    fi  
132 131
    if [ $verbose -gt 0 ]; then
133 132
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;

Also available in: Unified diff