Project

General

Profile

Revision 3ca6d126 test/test-compile.sh

View differences:

test/test-compile.sh
135 135
    popd > /dev/null
136 136
	# Cheching witness
137 137
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
139 139
    popd > /dev/null
140 140
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 141
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
169 169
	
170 170
    # Checking horn backend
171 171
    if [ "$main" != "" ]; then
172
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
172
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
173 173
    else
174
	$LUSTREC -horn -d $build -verbose 0 $opts "$name".lus
174
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
175 175
    fi
176 176
    if [ $? -ne 0 ]; then
177 177
        rlustrec="INVALID";

Also available in: Unified diff