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.580s | 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.614s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.645s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.659s | 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.580s | 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.691s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.658s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.738s | 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.674s | 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.721s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.672s | 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.660s | 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.705s | 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.548s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.472s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.568s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.488s | 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.580s | 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.863s | 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.971s | 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.721s | 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.910s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.705s | 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.784s | 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.612s | passed |
Standard output
1047887 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 1047887 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 1047887 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 1047887 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1052421 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 1052437 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1052452 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 1052562 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17554792245789109937.key 1052562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_17554792245789109937.key 1052562 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 1052562 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1057017 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 1057033 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_17554792245789109937.key 1057033 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1057142 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 1057142 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 1057142 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.9ns 1057142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1061832 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 1061864 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1061895 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.1ms 1062005 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14598873176514682281.key 1062005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_14598873176514682281.key 1062005 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.7ns 1062005 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1066836 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.84s 1066867 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_14598873176514682281.key 1066867 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 1066976 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8006138536159759421.key 1066976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_8006138536159759421.key 1066976 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.2ns 1066976 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1071557 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 1071588 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_8006138536159759421.key 1071588 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1071697 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1079281122205837511.key 1071697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1079281122205837511.key 1071697 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 1071697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1076466 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 1076497 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1079281122205837511.key 1076497 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1076607 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7646240112074288083.key 1076607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7646240112074288083.key 1076607 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.5ns 1076607 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1081171 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 1081203 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_7646240112074288083.key 1081203 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.6ns 1081312 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9718996675271174770.key 1081312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9718996675271174770.key 1081312 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239ns 1081312 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1085971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 1085987 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9718996675271174770.key 1085987 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 1086096 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_2970716081692590317.key 1086096 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_2970716081692590317.key 1086096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.8ns 1086096 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1090568 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 1090583 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2970716081692590317.key 1090583 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 1090708 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8476777418300827161.key 1090708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8476777418300827161.key 1090708 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239ns 1090708 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1095148 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 1095164 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_8476777418300827161.key 1095179 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ns 1095289 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 1095289 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 1095289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.8ns 1095289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1099778 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 1099793 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1099793 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 1099903 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15637890349223723545.key 1099903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15637890349223723545.key 1099903 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.8ns 1099903 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1104422 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 1104439 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15637890349223723545.key 1104439 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1104548 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11973736486100857942.key 1104548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_11973736486100857942.key 1104548 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.4ns 1104548 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1109066 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 1109082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_11973736486100857942.key 1109097 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 1109207 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16753923950280149646.key 1109207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_16753923950280149646.key 1109207 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.2ns 1109207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1113662 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 1113678 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_16753923950280149646.key 1113678 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 1113787 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15177698889614200792.key 1113787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_15177698889614200792.key 1113787 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.5ns 1113787 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1118353 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 1118369 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_15177698889614200792.key 1118369 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 1118479 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7370856722004869478.key 1118479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_7370856722004869478.key 1118479 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 1118479 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1122997 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 1123013 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_7370856722004869478.key 1123028 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 1123138 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15939403895187820287.key 1123138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_15939403895187820287.key 1123138 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 483.1ns 1123138 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1127735 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s 1127751 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_15939403895187820287.key 1127766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 1127876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2008466128081635211.key 1127876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2008466128081635211.key 1127876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.8ns 1127876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1132410 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 1132441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2008466128081635211.key 1132441 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1132550 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8470094350463508552.key 1132550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_8470094350463508552.key 1132550 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224ns 1132550 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1137131 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.59s 1137146 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_8470094350463508552.key 1137162 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 1137271 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11400284243555110730.key 1137271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11400284243555110730.key 1137271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.6ns 1137271 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1141805 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.53s 1141821 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11400284243555110730.key 1141821 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1141931 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12703631286622575877.key 1141931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_12703631286622575877.key 1141931 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.2ns 1141931 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1146511 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 1146527 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_12703631286622575877.key 1146527 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 1146636 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_1927636948427514850.key 1146636 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_1927636948427514850.key 1146636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.5ns 1146636 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1151045 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 1151076 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_1927636948427514850.key 1151076 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 1151185 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8106679926983666463.key 1151185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_8106679926983666463.key 1151185 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.6ns 1151185 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1155532 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1155547 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_8106679926983666463.key 1155547 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 1155657 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_5540247699991151617.key 1155657 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_5540247699991151617.key 1155657 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.1ns 1155657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1160100 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.44s 1160115 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_5540247699991151617.key 1160115 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 1160225 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9775580560413968568.key 1160225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9775580560413968568.key 1160225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.7ns 1160225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1164556 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1164603 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9775580560413968568.key 1164603 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns