MEM="-Xmx16G"

if [ "$#" -lt 4 ]; then
    echo "Error: Insufficient arguments provided." >&2
    echo "Usage: $0 <model.tla> <cinit> <strengthened_inv> <inv>" >&2
    echo "" >&2
    echo "Here, strengthened inv is a strengthening of inv with previously proven lemmas" >&2
    echo "It is your responsibility to prove them" >&2
    exit 1
fi

model="$1"
cinit="$2"
init_value="$3"
inv_value="$4"
set -x
JVM_ARGS=${MEM} apalache-mc check --cinit=${cinit} --init=Init --inv=$inv_value --length=0 ${model}
JVM_ARGS=${MEM} apalache-mc check --cinit=${cinit} --init=$init_value --inv=${inv_value} --length=1 ${model}