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] | 3.161s | 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] | 3.567s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 3.219s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 3.268s | 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] | 3.178s | 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] | 3.225s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 3.131s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 3.286s | 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] | 3.184s | 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] | 3.224s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 3.219s | 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] | 3.167s | 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] | 3.139s | 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] | 3.208s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 3.244s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 3.195s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 3.234s | 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] | 3.163s | 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] | 3.192s | 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] | 3.253s | 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] | 3.242s | 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] | 3.223s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 3.213s | 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] | 3.177s | passed |
| [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2) | testSMTLemmaSoundness(String, String)[9] | 3.197s | passed |
Standard output
756315 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 756315 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 756315 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.7ns 756315 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 759389 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 759404 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 759404 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 759520 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4053151836053499924.key 759520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4053151836053499924.key 759520 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.7ns 759520 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 762553 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 762569 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4053151836053499924.key 762569 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 762683 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 762683 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 762683 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 484ns 762683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 765719 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 765735 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 765766 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.86ms 765876 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16954734400532041232.key 765876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_16954734400532041232.key 765876 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.8ns 765876 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 768987 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 769018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_16954734400532041232.key 769018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 769129 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2274120807231446605.key 769129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_2274120807231446605.key 769129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.3ns 769129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 772241 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 772261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_2274120807231446605.key 772262 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 772371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_84654625658442690.key 772371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_84654625658442690.key 772371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.2ns 772371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 775469 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 775485 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_84654625658442690.key 775485 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 775594 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14927714487270973717.key 775594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_14927714487270973717.key 775594 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.7ns 775594 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 778681 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 778697 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_14927714487270973717.key 778697 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 778807 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2032835102784003720.key 778807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_2032835102784003720.key 778807 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.8ns 778807 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 781843 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 781859 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_2032835102784003720.key 781859 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 781984 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_15099138648648366580.key 781984 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_15099138648648366580.key 781984 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.8ns 781984 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 785056 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 785072 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_15099138648648366580.key 785072 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 785181 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8206300231342186172.key 785181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_8206300231342186172.key 785181 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.4ns 785181 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 788214 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 788230 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_8206300231342186172.key 788230 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 788342 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 788373 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 788373 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 560.9ns 788388 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 791561 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 791577 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 791796 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.96ms 791909 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3447941784431096996.key 791909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_3447941784431096996.key 791909 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 533.7ns 791909 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 795004 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 795020 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_3447941784431096996.key 795020 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 795129 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3983856705622021937.key 795129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_3983856705622021937.key 795129 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.6ns 795129 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 798271 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 798287 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_3983856705622021937.key 798287 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 798397 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7352611845453969160.key 798397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_7352611845453969160.key 798397 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.3ns 798397 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 801445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 801461 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_7352611845453969160.key 801461 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 801575 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14481248883065357932.key 801575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_14481248883065357932.key 801575 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.6ns 801575 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 804672 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 804687 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_14481248883065357932.key 804687 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 804800 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4170241754669282958.key 804800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_4170241754669282958.key 804800 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.1ns 804800 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 807801 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 807817 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_4170241754669282958.key 807817 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 807932 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9123259616985856896.key 807932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_9123259616985856896.key 807932 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.5ns 807932 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 811090 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 811105 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_9123259616985856896.key 811105 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 811218 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_725607136767335223.key 811218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_725607136767335223.key 811218 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.1ns 811218 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 814273 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 814288 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_725607136767335223.key 814288 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ns 814403 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4396001743901544484.key 814403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_4396001743901544484.key 814403 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.9ns 814403 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 817502 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 817517 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_4396001743901544484.key 817517 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 817627 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9109413303970895053.key 817627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_9109413303970895053.key 817627 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.1ns 817627 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 820653 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 820685 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_9109413303970895053.key 820685 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 820794 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14624404571774915392.key 820794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14624404571774915392.key 820794 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 423ns 820794 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 823804 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 823820 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14624404571774915392.key 823820 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 823933 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_16834043251870580460.key 823933 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_16834043251870580460.key 823933 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.8ns 823933 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 827016 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 827031 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_16834043251870580460.key 827031 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 827141 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9745114415711156292.key 827141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_9745114415711156292.key 827141 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.1ns 827141 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 830251 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 830267 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_9745114415711156292.key 830267 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 830385 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_14151606822866045020.key 830385 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_14151606822866045020.key 830385 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 459.4ns 830385 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 833448 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 833464 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_14151606822866045020.key 833464 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 833581 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2628749128001238809.key 833581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_2628749128001238809.key 833581 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.9ns 833581 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 836688 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 836704 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_2628749128001238809.key 836704 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns