Outputs comma-separated pairs of the form: "file.smt2, (A0, A1, ..., AN)" where As are the names of SMT assertions (set via the :named annotations).

z3-core.sh

#!/bin/bash

printf "$1,"
RESPONSE=$((
        (echo "(set-option :produce-unsat-cores true)"); 
        (echo "(set-option :smt.core.minimize true)");
        (cat $1); 
        (echo "(get-unsat-core)") 
) | z3 -smt2 -in)
if echo $RESPONSE | grep -q unknown; 
then
        >&2 echo Did not get Unsat Core from Z3, taking all named assertions instead;
        UNSAT_CORE=$(cat $1 | grep -oP ':named \K.*(?=\)\))' | tr "\n" " " | awk '{$1=$1};1')
        printf "($UNSAT_CORE)\n";
else
        echo ${RESPONSE#"unsat"};
fi