`get_model` returns SAT for UNSAT input

[PetarMax]

I ran into a problem in pyk when calling cterm_get_model, in that I am getting SAT back where I would expect UNSAT. The CTerm in question is:

CTerm(config=KApply(label=KLabel(name='<generatedTop>', params=()), args=(KApply(label=KLabel(name='<T>', params=()), args=(KApply(label=KLabel(name='<k>', params=()), args=(KVariable(name='K_CELL', sort=None),)), KApply(label=KLabel(name='<state>', params=()), args=(KVariable(name='STATE_CELL', sort=None),)))), KApply(label=KLabel(name='<generatedCounter>', params=()), args=(KVariable(name='GENERATEDCOUNTER_CELL', sort=None),)))), constraints=(KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='true', sort=KSort(name='Bool')), KApply(label=KLabel(name='_<Int_', params=()), args=(KVariable(name='N', sort=KSort(name='Int')), KToken(token='15', sort=KSort(name='Int')))))), KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='true', sort=KSort(name='Bool')), KApply(label=KLabel(name='_>Int_', params=()), args=(KVariable(name='N', sort=KSort(name='Int')), KToken(token='10', sort=KSort(name='Int')))))), KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='true', sort=KSort(name='Bool')), KApply(label=KLabel(name='notBool_', params=()), args=(KApply(label=KLabel(name='_andBool_', params=()), args=(KApply(label=KLabel(name='_==K_', params=()), args=(KSequence(items=()), KSequence(items=()))), KApply(label=KLabel(name='_==K_', params=()), args=(KApply(label=KLabel(name='_|->_', params=()), args=(KToken(token='$n', sort=KSort(name='Id')), KApply(label=KLabel(name='_+Int_', params=()), args=(KVariable(name='N', sort=KSort(name='Int')), KVariable(name='N', sort=KSort(name='Int')))))), KApply(label=KLabel(name='_|->_', params=()), args=(KToken(token='$n', sort=KSort(name='Id')), KApply(label=KLabel(name='_*Int_', params=()), args=(KToken(token='2', sort=KSort(name='Int')), KVariable(name='N', sort=KSort(name='Int')))))))))),))))))

or in kore:

And(sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=App(symbol="Lbl'-LT-'generatedTop'-GT-'", sorts=(), args=(App(symbol="Lbl'-LT-'T'-GT-'", sorts=(), args=(App(symbol="Lbl'-LT-'k'-GT-'", sorts=(), args=(EVar(name="VarK'Unds'CELL", sort=SortApp(name='SortK', sorts=())),)), App(symbol="Lbl'-LT-'state'-GT-'", sorts=(), args=(EVar(name="VarSTATE'Unds'CELL", sort=SortApp(name='SortMap', sorts=())),)))), App(symbol="Lbl'-LT-'generatedCounter'-GT-'", sorts=(), args=(EVar(name="VarGENERATEDCOUNTER'Unds'CELL", sort=SortApp(name='SortInt', sorts=())),)))), right=And(sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=Equals(op_sort=SortApp(name='SortBool', sorts=()), sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=DV(sort=SortApp(name='SortBool', sorts=()), value=String(value='true')), right=App(symbol="Lbl'Unds-LT-'Int'Unds'", sorts=(), args=(EVar(name='VarN', sort=SortApp(name='SortInt', sorts=())), DV(sort=SortApp(name='SortInt', sorts=()), value=String(value='15'))))), right=And(sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=Equals(op_sort=SortApp(name='SortBool', sorts=()), sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=DV(sort=SortApp(name='SortBool', sorts=()), value=String(value='true')), right=App(symbol="Lbl'Unds-GT-'Int'Unds'", sorts=(), args=(EVar(name='VarN', sort=SortApp(name='SortInt', sorts=())), DV(sort=SortApp(name='SortInt', sorts=()), value=String(value='10'))))), right=Equals(op_sort=SortApp(name='SortBool', sorts=()), sort=SortApp(name='SortGeneratedTopCell', sorts=()), left=DV(sort=SortApp(name='SortBool', sorts=()), value=String(value='true')), right=App(symbol="LblnotBool'Unds'", sorts=(), args=(App(symbol="Lbl'Unds'andBool'Unds'", sorts=(), args=(App(symbol="Lbl'UndsEqlsEqls'K'Unds'", sorts=(), args=(App(symbol='dotk', sorts=(), args=()), App(symbol='dotk', sorts=(), args=()))), App(symbol="Lbl'UndsEqlsEqls'K'Unds'", sorts=(), args=(App(symbol='inj', sorts=(SortApp(name='SortMap', sorts=()), SortApp(name='SortK', sorts=())), args=(App(symbol="Lbl'UndsPipe'-'-GT-Unds'", sorts=(), args=(App(symbol='inj', sorts=(SortApp(name='SortId', sorts=()), SortApp(name='SortKItem', sorts=())), args=(DV(sort=SortApp(name='SortId', sorts=()), value=String(value='$n')),)), App(symbol='inj', sorts=(SortApp(name='SortInt', sorts=()), SortApp(name='SortKItem', sorts=())), args=(App(symbol="Lbl'UndsPlus'Int'Unds'", sorts=(), args=(EVar(name='VarN', sort=SortApp(name='SortInt', sorts=())), EVar(name='VarN', sort=SortApp(name='SortInt', sorts=())))),)))),)), App(symbol='inj', sorts=(SortApp(name='SortMap', sorts=()), SortApp(name='SortK', sorts=())), args=(App(symbol="Lbl'UndsPipe'-'-GT-Unds'", sorts=(), args=(App(symbol='inj', sorts=(SortApp(name='SortId', sorts=()), SortApp(name='SortKItem', sorts=())), args=(DV(sort=SortApp(name='SortId', sorts=()), value=String(value='$n')),)), App(symbol='inj', sorts=(SortApp(name='SortInt', sorts=()), SortApp(name='SortKItem', sorts=())), args=(App(symbol="Lbl'UndsStar'Int'Unds'", sorts=(), args=(DV(sort=SortApp(name='SortInt', sorts=()), value=String(value='2')), EVar(name='VarN', sort=SortApp(name='SortInt', sorts=())))),)))),)))))),))))))

or (somewhat) pretty-printed:

<generatedTop>
  <T>
    <k>
      K_CELL
    </k>
    <state>
      STATE_CELL
    </state>
  </T>
  <generatedCounter>
    GENERATEDCOUNTER_CELL
  </generatedCounter>
</generatedTop>
#And { true #Equals N:Int <Int 15 }
#And { true #Equals N:Int >Int 10 }
#And { true #Equals notBool .K ==K .K andBool $n |-> N:Int +Int N:Int ==K $n |-> 2 *Int N:Int }

which is not satisfiable, since the third constraint does not hold (separately, the print is not correct, since notBool extends to both conjuncts (should be notBool ( .K ==K .K andBool $n |-> N:Int +Int N:Int ==K $n |-> 2 *Int N:Int )).

The substitution I get that supposedly satisfies this is N = 11.

Specifically, the call that is done is: result = kore_client.get_model(kore) where the kore holds the above kore term.