Cannot evaluate simple predicate without SMT solver

[ehildenb]

kevm-bug.tar.gz

This file comes from a simple proof on https://github.com/kframework/evm-semantics/pull/912/commits/06c9c8b514b544057e27a81e568acd89eda58654.

The proof is from tests/specs/functional/lemmas-no-smt-spec.k, and looks like this:

    claim <k> runLemma ( 1 ==Int bool2Word( B:Bool ) )   => doneLemma ( B ==K true ) ... </k>

The error produced looks like this:

kore-exec: [2886042] Error (ErrorDecidePredicateUnknown):
    Failed to decide predicate:            
        /* Sfa */
        \not{R}(
            /* Spa */
            \equals{SortBool{}, R}(
                /* Fl Fn D Sfa */ VarB:SortBool{},
                /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortBool{}}("false")
            )
        )
    with side condition:
        /* D Sfa */ \top{_PREDICATE{}}()

[ttuegel]

@ehildenb Can you confirm that the evm-semantics build system still runs this spec without the SMT solver?

[ehildenb]

@ttuegel yes the build system passes --haskell-backend-command 'kore-exec --smt=none', and if you look at kore-exec.sh, you can see the --smt none option. Anything else you'd like me to verify about that?

[ttuegel]

This was probably triggered by #2170 and would be fixed by #2174. I need to investigate that, but that's where I'll start.

[ana-pantilie]

What I've found so far is that during the application of this equation, we send the condition to the solver when we check the requires, here, and this is what triggers the error because we're running this test without the solver.

[ttuegel]

I'm can't really explain how this ever worked. The cited rule requires the SMT solver to be applied. My hope for fixing this right now is that, as part of #1986, the backend will apply simplification rules before and after function definitions, so we can avoid that rule with the appropriate lemma.