ProveSMTLemmasTest
|
100%
successful |
Tests
| Test | Method name | Duration | Result |
|---|---|---|---|
| [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null) | testSMTLemmaSoundness(String, String)[10] | 4.123s | passed |
| [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1)) | testSMTLemmaSoundness(String, String)[11] | 4.132s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.052s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.136s | passed |
| [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi)) | testSMTLemmaSoundness(String, String)[14] | 4.107s | passed |
| [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1)))) | testSMTLemmaSoundness(String, String)[15] | 4.073s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.125s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.102s | passed |
| [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE ) | testSMTLemmaSoundness(String, String)[18] | 4.112s | passed |
| [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[19] | 4.508s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.378s | passed |
| [20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f)) | testSMTLemmaSoundness(String, String)[20] | 4.266s | passed |
| [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2)) | testSMTLemmaSoundness(String, String)[21] | 4.177s | passed |
| [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0) | testSMTLemmaSoundness(String, String)[22] | 4.264s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.215s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.280s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.135s | passed |
| [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside) | testSMTLemmaSoundness(String, String)[2] | 4.270s | passed |
| [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside ) | testSMTLemmaSoundness(String, String)[3] | 4.345s | passed |
| [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 ) | testSMTLemmaSoundness(String, String)[4] | 4.299s | passed |
| [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f)) | testSMTLemmaSoundness(String, String)[5] | 4.299s | passed |
| [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 ) | testSMTLemmaSoundness(String, String)[6] | 4.325s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.126s | passed |
| [8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) ) | testSMTLemmaSoundness(String, String)[8] | 4.188s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 4.187s | passed |
Standard output
1028704 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 1028704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jmod.dl.proof 1028704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 1028722 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1032946 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 1032977 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1032977 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 1033086 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15791832126735963459.key 1033086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_15791832126735963459.key 1033086 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.9ns 1033086 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1037216 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1037247 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_15791832126735963459.key 1037247 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 1037356 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 1037356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_seqGetOutside.dl.proof 1037356 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 507.7ns 1037356 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1041543 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1041559 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1041590 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.8ms 1041701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5669249547966670714.key 1041701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5669249547966670714.key 1041701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.5ns 1041701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1045870 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1045886 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5669249547966670714.key 1045886 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 1046000 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8608915111090884542.key 1046000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8608915111090884542.key 1046000 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 288ns 1046000 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1050172 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 1050188 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8608915111090884542.key 1050188 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 1050299 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10719650837652889201.key 1050299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_10719650837652889201.key 1050299 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.9ns 1050299 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1054497 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 1054512 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_10719650837652889201.key 1054512 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 1054624 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16220663205686036468.key 1054624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_16220663205686036468.key 1054624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.3ns 1054624 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1058610 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 1058625 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_16220663205686036468.key 1058641 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 1058750 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16547457245758301544.key 1058750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_16547457245758301544.key 1058750 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.1ns 1058750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1062813 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1062829 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_16547457245758301544.key 1062829 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 1062938 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_9661514087859574614.key 1062938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl.2_9661514087859574614.key 1062938 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.2ns 1062938 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1066996 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 1067011 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_9661514087859574614.key 1067011 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 1067126 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15292876200313257119.key 1067126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_15292876200313257119.key 1067126 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.7ns 1067126 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1071109 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 1071124 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_15292876200313257119.key 1071140 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 1071249 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 1071249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\smt\newsmt2\SMT_lemma_jdiv.dl.proof 1071249 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 181ns 1071249 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1075240 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 1075256 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1075256 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 1075381 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_10612177011868545216.key 1075381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_10612177011868545216.key 1075381 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.5ns 1075381 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1079308 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 1079323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_10612177011868545216.key 1079323 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 1079433 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8080703783571284035.key 1079433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_8080703783571284035.key 1079433 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.4ns 1079433 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1083428 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 1083444 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_8080703783571284035.key 1083444 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 1083569 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1309980846229453573.key 1083569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_1309980846229453573.key 1083569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.6ns 1083569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1087532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 1087563 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_1309980846229453573.key 1087563 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ns 1087676 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9389956018379384296.key 1087676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_9389956018379384296.key 1087676 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.4ns 1087676 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1091608 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.94s 1091640 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_9389956018379384296.key 1091640 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 1091749 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7810635592710072440.key 1091749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7810635592710072440.key 1091749 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.9ns 1091749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1095734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 1095750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7810635592710072440.key 1095766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ns 1095875 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15294988906050494313.key 1095875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15294988906050494313.key 1095875 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.1ns 1095875 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1099851 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 1099867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15294988906050494313.key 1099867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ns 1099978 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13393107863939197559.key 1099978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_13393107863939197559.key 1099978 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.4ns 1099978 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1103960 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 1103976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_13393107863939197559.key 1103976 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ns 1104090 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10296720291869170432.key 1104090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_10296720291869170432.key 1104090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.9ns 1104090 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1108467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s 1108483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_10296720291869170432.key 1108483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.4ns 1108598 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11684321262506297128.key 1108598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11684321262506297128.key 1108598 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.2ns 1108598 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1112734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1112749 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11684321262506297128.key 1112749 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ns 1112864 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1561484903553891509.key 1112864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_1561484903553891509.key 1112864 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.1ns 1112864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1116900 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1116916 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_1561484903553891509.key 1116916 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 1117041 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_1942753546402420804.key 1117041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl.2_1942753546402420804.key 1117041 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.4ns 1117041 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1121178 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 1121194 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1942753546402420804.key 1121194 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 1121305 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_852844260601116972.key 1121305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_852844260601116972.key 1121305 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.7ns 1121305 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1125395 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 1125410 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_852844260601116972.key 1125410 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 1125520 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_6664996628455561750.key 1125520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl.2_6664996628455561750.key 1125520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 1125520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1129659 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.14s 1129675 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_6664996628455561750.key 1129691 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 1129800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3341787010456706708.key 1129800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_3341787010456706708.key 1129800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.2ns 1129800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1133795 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 1133810 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_3341787010456706708.key 1133826 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns