From 65599f14b3ecac193529caafbee7672b38ed367e Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 15 Feb 2019 03:04:37 +0000 Subject: Use multiple solvers Useful to see what constraints we are generating that are particularly hard, and which of our specs work with different solvers. Refactor code to use smt in names rather than specifically z3 --- test/typecheck/run_tests.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test') diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh index ad2592df..e5650646 100755 --- a/test/typecheck/run_tests.sh +++ b/test/typecheck/run_tests.sh @@ -50,9 +50,9 @@ printf "\n" >> $DIR/tests.xml for i in `ls $DIR/pass/ | grep sail`; do - if $SAILDIR/sail -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i; + if $SAILDIR/sail -no_memo_z3 -just_check -ddump_tc_ast -dsanity $DIR/pass/$i 2> /dev/null 1> $DIR/rtpass/$i; then - if $SAILDIR/sail -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i; + if $SAILDIR/sail -no_memo_z3 -just_check -ddump_tc_ast -dmagic_hash -dno_cast -dsanity $DIR/rtpass/$i 2> /dev/null 1> $DIR/rtpass2/$i; then if diff $DIR/rtpass/$i $DIR/rtpass2/$i; then @@ -71,7 +71,7 @@ do for file in $DIR/pass/${i%.sail}/*.sail; do pushd $DIR/pass > /dev/null; - if $SAILDIR/sail ${i%.sail}/$(basename $file) 2> result; + if $SAILDIR/sail -no_memo_z3 ${i%.sail}/$(basename $file) 2> result; then red "failing variant of $i $(basename $file) passed" "fail" else -- cgit v1.2.3