Proving Specs in K 4.0

[ZhuXiaoran07]

I am trying to prove sth. about arrays. The semantics is much like imp.k except adding some rules about arrays:

`

syntax Int ::="["Id "," AExp "]"
syntax Int::= "value-array" "(" Int ")" [function]

syntax Int::= "update" "(" Id "," Int "," Int ")"
syntax Map::=	"array-map" "(" Int "," Int ")" [function]

rule T:Type X:Id[I:Int];=>[X,I]...
M:Map
when notBool(I in keys(M))

rule T:Type X:Id[I:Id];=> [X, I']...
...I|->N...
...N|->I':Int...

rule array-map(I, L)=>(value-array(L-Int 1)|->0) array-map(I, L-Int 1)
requires L>Int 0

rule array-map(I, 0)=>.Map

rule ([X, I]=>.) ...
AE:Bag=>AE 
X:Id 
array-map(I,I) 

T=>T+Int 1

rule X:Id[I1:Int]=I2=>update(X,I1,I2)

rule <k>update(X,I1,I2)=>I2...</k>
<arrayEnv>
				  <arrayId> X:Id </arrayId>
				  <arrayStore>M:Map value-array(I1)|->(_=>I2) </arrayStore>
				  </arrayEnv>
<time> T=>T+Int 1 </time>


rule <k>(X:Id[I1]=>I2:Int)...</k>
<arrayEnv>
		 <arrayId> X:Id </arrayId>
		<arrayStore>... value-array(I1)|->I2 ...</arrayStore>
				  </arrayEnv>

The program to be proved:

int n; int i; print("The length of the array:"); 
n=read(); 
int a[n]; 
while(i<n){ 
a[i]=i; 
i=i+1; }

And the spec of this program:

rule <k>
 while(i< n- 1){
 a[i]=i; 
i=i+ 1; } 
=>.K ... 
</k>
 <arrayEnvs> 
<arrayEnv> 
<arrayId>a</arrayId>
 <arrayStore>M:Map=>?_:Map</arrayStore>
 </arrayEnv> </arrayEnvs>
 <env> ... n|->LN:Int i|->LI:Int ... </env>
 <store> ... LN|->N:Int LI|->(_:Int=>?I':Int) ... </store>
 <time> T:Int=>?T':Int </time>
 requires N>Int 0 
ensures ?T'>Int T

This spec could be proved correctly in K3.6, while I got an error trace when proving it in K 4.0:

`java.lang.UnsupportedOperationException: missing SMTLib translation for #KSequence
at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:490)
at org.kframework.backend.java.kil.KItem.accept(KItem.java:743)
at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:611)
at org.kframework.backend.java.kil.BuiltinList.accept(BuiltinList.java:252)
at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:244)
at org.kframework.backend.java.symbolic.KILtoSMTLib.translateTerm(KILtoSMTLib.java:457)
at org.kframework.backend.java.symbolic.KILtoSMTLib.transform(KILtoSMTLib.java:431)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.accept(ConjunctiveFormula.java:815)
at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:244)
at org.kframework.backend.java.symbolic.KILtoSMTLib.translateImplication(KILtoSMTLib.java:192)
at org.kframework.backend.java.symbolic.SMTOperations.impliesSMT(SMTOperations.java:61)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.impliesSMT(ConjunctiveFormula.java:725)
at org.kframework.backend.java.symbolic.ConjunctiveFormula.implies(ConjunctiveFormula.java:669)
at org.kframework.backend.java.kil.ConstrainedTerm.matchImplies(ConstrainedTerm.java:160)
at org.kframework.backend.java.symbolic.SymbolicRewriter.applySpecRules(SymbolicRewriter.java:654)
at org.kframework.backend.java.symbolic.SymbolicRewriter.proveRule(SymbolicRewriter.java:589)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.lambda$prove$152(InitializeRewriter.java:203)
at java.util.stream.ReferencePipeline$3$1.accept(Unknown Source)
at java.util.stream.ReferencePipeline$2$1.accept(Unknown Source)
at java.util.ArrayList$ArrayListSpliterator.forEachRemaining(Unknown Source)
at java.util.stream.AbstractPipeline.copyInto(Unknown Source)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(Unknown Source)
at java.util.stream.ReduceOps$ReduceOp.evaluateSequential(Unknown Source)
at java.util.stream.AbstractPipeline.evaluate(Unknown Source)
at java.util.stream.ReferencePipeline.collect(Unknown Source)
at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.prove(InitializeRewriter.java:205)
at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:165)
at org.kframework.backend.java.symbolic.ProofExecutionMode.execute(ProofExecutionMode.java:54)
at org.kframework.krun.KRun.run(KRun.java:86)
at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:97)
at org.kframework.main.FrontEnd.main(FrontEnd.java:52)
at org.kframework.main.Main.runApplication(Main.java:110)
at org.kframework.main.Main.runApplication(Main.java:100)
at org.kframework.main.Main.main(Main.java:52)
(error "line 7 column 73: unknown function/constant smt_seq_elem")
(error "line 6 column 24: unknown sort 'IntSeq'")
(error "line 7 column 56: unknown constant _148823")
(error "line 7 column 65: invalid function application for =, sort mismatch on argument at position 2, expected K but given Int")
(error "line 4 column 16: unexpected character")
(error "line 7 column 56: unknown constant R_I")
(error "line 7 column 59: unexpected character")
(error "line 7 column 60: invalid function application for =, sort mismatch on argument at position 2, expected K but given Int")
(error "line 7 column 77: unknown function/constant smt_seq_elem")
[Error] Internal: Uncaught exception thrown of type AssertionError.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues
[Warning] Critical: failed to translate smtlib expression:
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun _148731 () Bool)
(assert (and (= (< _627 (- _10684 1)) true) (= _148731 true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun _148736 () Bool)
(assert (and (= (< _627 (- _10684 1)) true) (= _148736 true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun R_I2 () Int)
(declare-fun _10684 () Int)
(declare-fun _148896 () Bool)
(declare-fun _148895 () K)
(assert (and (= (< _627 (- _10684 1)) false) (= _148895 R_I2) (= _148896
true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun R_I () Int)
(declare-fun _148784 () Bool)
(declare-fun _148783 () K)
(assert (and (= (< _627 (- _10684 1)) false) (= _148783 (smt_seq_elem R_I)) (=
_148784 true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun R_I () Int)
(declare-fun _148850 () Bool)
(declare-fun _148849 () K)
(assert (and (= (< _627 (- _10684 1)) false) (= _148849 (+ R_I 1)) (= _148850
true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun R_I' () Int)
(declare-fun _148857 () Bool)
(declare-fun _148856 () K)
(assert (and (= (< _627 (- _10684 1)) false) (= _148856 R_I') (= _148857
true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun _148737 () Bool)
(declare-fun _186 () Int)
(declare-fun _189 () K)
(assert (and (and (= (< _627 (- _10684 1)) false) (= _148737 true)) (not (and
(= _189 _189) (= (> (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ _186 1) 1) 1) 1) 1)

_186) true)))))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _10684 () Int)
(declare-fun _148824 () Bool)
(declare-fun _148822 () K)
(declare-fun _148823 () IntSeq)
(assert (and (= (< _627 (- _10684 1)) false) (= _148822 _148823) (= _148824
true)))
[Warning] Critical: failed to translate smtlib expression:
(declare-sort K)
(declare-fun _627 () Int)
(declare-fun _149048 () Int)
(declare-fun _10684 () Int)
(declare-fun _149054 () Bool)
(declare-fun _149053 () K)
(assert (and (= (< _627 (- _10684 1)) false) (= _149053 (smt_seq_elem _149048))
(= _149054 true)))`