krun --smt none makes all smt queries crash the execution

[dwightguth]

I'll add an example I can guarantee will reproduce the error when I get home, but I think you can probably reproduce this with any execution of kore-exec which triggers the smt solver to try to decide a predicate.

To summarize, if you pass --smt none to krun when using the haskell backend, and it tries to decide a predicate using an smt solver, it appears to currently trigger a "failed to decide predicate" error, when in fact what we'd really like is if it branches on the predicate.

[dwightguth]

I can't currently guarantee since I'm away from my computer, but I think this will trigger the error:

module TEST
imports INT
syntax Type ::= "a" | "b"
syntax Exp ::= Type "=" Type
rule 0 => ?T1:Type = ?T2:Type
rule T = T => .
endmodule

kompile test.k --backend haskell
krun -cPGM=0 --smt none

[dwightguth]

I confirmed this example does indeed reproduce the following crash:

kore-exec: [150221] Error (DecidePredicateUnknown):
    Failed to decide predicate:
        /* Sfa */
        \not{_}(
            /* Spa */
            \equals{SortType{}, _}(
                /* Fl Fn D Sfa */ Var'Ques'T1:SortType{},
                /* Fl Fn D Sfa */ Var'Ques'T2:SortType{}
            )
        )
    SMT limit set at:
        0
Context:
    (DebugEvaluateCondition) while evaluating predicate
        (DecidePredicateUnknown) while applying equation
                                 in Kore.Rewrite:201:74
Created bug report: kore-exec.tar.gz
[Error] krun: kore-exec ./test-kompiled/haskellDefinition.bin --module TEST
--pattern .krun-2023-02-16-14-49-38-lZG0fDMRk8/tmp.in.NAUq0ZHi23 --output
.krun-2023-02-16-14-49-38-lZG0fDMRk8/result.kore --smt none
[Error] krun: Backend crashed during rewriting with exit code 1

I would really rather it simply branch on whether ?T1 and ?T2 are equal.