#!/bin/sh

# test the SMT-LIB parser

PRI=../../princess

TESTS="bignum_quant.smt2 \
       int_incompleteness1.smt2 int_incompleteness2.smt2 \
       int_incompleteness3.smt2 \
       init-1.smt2 MULTIPLIER_2.msat.smt2 \
       ite.smt2 ite2.smt2 ite3.smt2 \
       for_in_term.smt2 for_in_term2.smt2 \
       let.smt2 let2.smt2 \
       divmod.smt2 arrays.smt2 arrays2.smt2 arrays3.smt2 \
       patternBug.smt2 correct-eq.smt2 \
       array-interpolation.smt2 \
       define-fun.smt2 define-fun2.smt2 define-fun3.smt2 \
       define-fun-interpolation.smt2 \
       multiple-check-sat.smt2 seconds.smt2 \
       quotes.smt2 extensions.smt2 boolean-quant.smt2 \
       simple-joogie.smt2"

$PRI "$@" $TESTS

$PRI "$@" +boolFunsAsPreds changing_truth_value_unsafe_garbage.c.smt2
