Unable to narrow on results of uninterpretted functions

[nishantjr]

The following definition crashes with (ErrorRewritesInstantiation)

module TEST
    imports BOOL
    imports INT

    syntax MaybeInt ::= "Some" Int
                      | "None"
    syntax MaybeInt ::= f() [function, functional, no-evaluators]

    configuration <k> f() </k>

    rule <k> None => true ... </k>
    rule <k> Some I => I ... </k>
endmodule

We expect it to narrow to two cases:

• one with f() ==K None and the K cell contains true
• one where f() :=K Some I:Int and the K cell contains I

[ttuegel]

We should change this check so that any configuration that is not "constructor-like" is considered symbolic for the purpose of allowing narrowing.