Project

General

Profile

Revision 4437ddbc 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 2>/dev/null
119
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus -verbose 0
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

Also available in: Unified diff