Project

General

Profile

Revision 59294251 test/test-compile.sh

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