#!/bin/sh

# Some examples that need special settings

PRI=../../princess

$PRI "$@" -simplifyConstraints=lemmas -posUnitResolution functions2b.pri
$PRI "$@" -posUnitResolution tarskiGeometry2.pri
$PRI "$@" -timeout=30000 -clausifier=none +posUnitResolution group0.pri
$PRI "$@" -timeout=30000 +posUnitResolution -constructProofs=always counterExampleBug.pri
$PRI "$@" -timeout=30000 -constructProofs=always omega_problem__031.smt.pri | grep -v "^Certificate" | grep -v "^Assumed"
$PRI "$@" -generateTriggers=total -genTotalityAxioms +reverseFunctionalityPropagation -tightFunctionScopes ricart-agrawala7.smt2
$PRI "$@" -timeout=15000 proofBug.pri
$PRI "$@" -timeout=15000 multiplication3.pri
$PRI "$@" -generateTriggers=total -timeout=60000 vstte-problem-2-vc.pri
$PRI "$@" -timeout=30000 -generateTriggers=all +mostGeneralConstraint soldiers.pri
