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.444s | 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.454s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.453s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.458s | 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.477s | 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.477s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.464s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.461s | 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.467s | 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.441s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.488s | 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.458s | 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.474s | 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.455s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.437s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.476s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.447s | 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.487s | 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.444s | 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.431s | 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.457s | 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.412s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.432s | 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.424s | 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.409s | passed |
Standard output
1016181 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 1016181 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 1016181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 1016197 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1020533 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1020549 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 1020565 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 1020674 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10094793135303553552.key 1020674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_10094793135303553552.key 1020674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.7ns 1020674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1025020 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1025036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_10094793135303553552.key 1025036 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 1025161 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 1025161 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 1025161 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.6ns 1025161 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1029462 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1029477 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 1029493 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 1029605 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5324366373969924179.key 1029605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_5324366373969924179.key 1029605 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.6ns 1029605 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1033907 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1033923 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_5324366373969924179.key 1033923 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 1034036 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10393582336760140526.key 1034036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_10393582336760140526.key 1034036 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.9ns 1034036 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1038352 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1038368 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_10393582336760140526.key 1038368 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 1038493 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1235450893276758911.key 1038493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_1235450893276758911.key 1038493 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.7ns 1038493 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1042779 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1042795 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_1235450893276758911.key 1042795 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 1042905 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11467810526780459042.key 1042905 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_11467810526780459042.key 1042905 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.6ns 1042905 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1047208 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 1047223 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_11467810526780459042.key 1047223 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ns 1047337 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13126610473818725560.key 1047337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_13126610473818725560.key 1047337 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.6ns 1047337 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1051636 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1051652 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_13126610473818725560.key 1051652 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ns 1051761 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_10139461667097354358.key 1051761 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_10139461667097354358.key 1051761 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.5ns 1051761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1056040 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 1056056 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_10139461667097354358.key 1056056 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ns 1056170 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13451443731737666899.key 1056170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_13451443731737666899.key 1056170 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.5ns 1056170 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1060453 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 1060484 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_13451443731737666899.key 1060500 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 1060614 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 1060614 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 1060614 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.4ns 1060614 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1064940 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1064955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 1064955 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 996.4ns 1065068 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8310730391432361414.key 1065068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_8310730391432361414.key 1065068 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.4ns 1065068 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1069380 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1069396 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_8310730391432361414.key 1069396 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 1069521 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15775066239572647558.key 1069521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_15775066239572647558.key 1069521 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 1069521 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1073838 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1073854 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_15775066239572647558.key 1073869 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ns 1073979 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14057331129689258007.key 1073979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_14057331129689258007.key 1073979 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.1ns 1073979 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1078323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1078339 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_14057331129689258007.key 1078339 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 1078456 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10049086566831527347.key 1078456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_10049086566831527347.key 1078456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 1078456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1082808 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 1082823 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_10049086566831527347.key 1082823 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 1082933 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8423055454971935886.key 1082933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_8423055454971935886.key 1082933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.5ns 1082933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1087273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 1087288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_8423055454971935886.key 1087288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ns 1087398 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13238248982760589569.key 1087398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_13238248982760589569.key 1087398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.5ns 1087398 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1091734 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1091750 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_13238248982760589569.key 1091750 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 1091859 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4783586396380321361.key 1091859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_4783586396380321361.key 1091859 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.8ns 1091859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1096201 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 1096216 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_4783586396380321361.key 1096216 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 1096326 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6636514945719410562.key 1096326 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_6636514945719410562.key 1096326 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.1ns 1096326 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1100642 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1100657 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_6636514945719410562.key 1100657 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ns 1100767 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14332995701985114233.key 1100767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_14332995701985114233.key 1100767 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.9ns 1100767 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1105096 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1105112 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_14332995701985114233.key 1105112 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 1105225 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17688017862109026380.key 1105225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_17688017862109026380.key 1105225 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.9ns 1105225 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1109558 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 1109574 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_17688017862109026380.key 1109574 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ns 1109699 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_11346983188047478160.key 1109699 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_11346983188047478160.key 1109699 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 1109699 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1114030 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 1114046 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_11346983188047478160.key 1114046 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 1114155 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15555803406817613924.key 1114155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_15555803406817613924.key 1114155 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.3ns 1114155 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1118467 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 1118483 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_15555803406817613924.key 1118483 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ns 1118593 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_3584451117807141028.key 1118593 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_3584451117807141028.key 1118593 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.7ns 1118593 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1122939 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.34s 1122955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_3584451117807141028.key 1122955 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 1123069 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9200412180569417330.key 1123069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_9200412180569417330.key 1123069 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.8ns 1123069 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1127388 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 1127404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_9200412180569417330.key 1127404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns