#!/bin/sh

PRI=../../princess

TESTS="columnRed.pri cryptarithm.pri \
       eqProof2.pri eqProof3.pri eqProof4.pri eqProof5.pri \
       eqProof6.pri eqProof.pri \
       surprising.pri \
       inEqProof0.pri inEqProof1.pri inEqProof2.pri \
       inEqProof3.pri inEqProof.pri \
       int_incompleteness2.pri int_incompleteness3.pri \
       pidgeon.pri pidgeonSimplified.pri pidgeonSuperSimplified.pri \
       prog.pri \
       prop0.pri prop1.pri prop2.pri prop3.pri prop4.pri prop5.pri \
       queen2-1.pri queen3-1.pri \
       super_queen2-1.pri super_queen3-1.pri \
       cav-ex4b.pri quan.pri ring_2exp10_3vars_2ite_unsat.pri \
       arrays0.pri constOrderBug.pri strange_concurrency.pri \
       wrongInterpolant3.pri omegaBug.pri splitEq.pri \
       incorrectPredInterpolant.pri certificateBug.pri \
       missingOmegaSupport.pri bignum_lia1.pri \
       linear-combination-bug.pri div-right-bug.pri \
       tree.pri"

#       super_queen4-1.pri super_queen5-1.pri super_queen6-1.pri super_queen7-1.pri \

$PRI "$@" $TESTS

# Some examples that need special settings.

# Testing some large examples for which we have to switch off assertions

TESTS="prp-2-17.pri prp-3-18.pri"

$PRI "$@" -assert $TESTS

# We switch off quantifier elimination in interpolants for those
# examples, as well as assertions (because just checking that
# the interpolants are correct takes too long)

TESTS="surprising25.pri bignum_lia1.pri"

$PRI "$@" -elimInterpolantQuants -simplifyProofs -assert $TESTS

# Testing proof simplification

$PRI "$@" +simplifyProofs -constructProofs=always ring_2exp10_3vars_0ite_unsat.pri | grep -v "^Certificate" | grep -v "^Assumed"
