File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -194,7 +194,7 @@ strip_solver_mode_flags() {
194194
195195if [ " $binary " = yices_smt2 ] && [[ " $test_file " == * " /both/" * ]]; then
196196 options=$( strip_solver_mode_flags " $options " )
197- test_string=" $test_file [ $options --mcsat ] [ $options --dpllt ]"
197+ test_string=" $test_file [ $options --mcsat ] [ $options ]"
198198
199199 outfile2=$( $mktemp_cmd ) || { echo " Can't create temp file" ; rm -f " $timefile " " $outfile " ; exit 3 ; }
200200 timefile2=$( $mktemp_cmd ) || { echo " Can't create temp file" ; rm -f " $timefile " " $outfile " " $outfile2 " ; exit 3 ; }
@@ -205,7 +205,7 @@ if [ "$binary" = yices_smt2 ] && [[ "$test_file" == *"/both/"* ]]; then
205205 diff_mcsat=$( diff -w " $outfile " " $gold " )
206206 diff_status_mcsat=$?
207207
208- run_solver_once " $options --dpllt " " $outfile2 " " $timefile2 "
208+ run_solver_once " $options " " $outfile2 " " $timefile2 "
209209 status_dpllt=$?
210210 runtime_dpllt=$( cat " $timefile2 " )
211211 diff_dpllt=$( diff -w " $outfile2 " " $gold " )
You can’t perform that action at this time.
0 commit comments