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.144s | 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.110s | passed |
| [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false ) | testSMTLemmaSoundness(String, String)[12] | 4.127s | passed |
| [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true ) | testSMTLemmaSoundness(String, String)[13] | 4.129s | 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.160s | 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.133s | passed |
| [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0 | testSMTLemmaSoundness(String, String)[16] | 4.170s | passed |
| [17] length.dl, \forall Object o; length(o) >= 0 | testSMTLemmaSoundness(String, String)[17] | 4.148s | 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.149s | 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.181s | passed |
| [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom | testSMTLemmaSoundness(String, String)[1] | 4.215s | 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.137s | 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.167s | 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.144s | passed |
| [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x | testSMTLemmaSoundness(String, String)[23] | 4.196s | passed |
| [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1 | testSMTLemmaSoundness(String, String)[24] | 4.198s | passed |
| [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null) | testSMTLemmaSoundness(String, String)[25] | 4.132s | 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.182s | 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.265s | 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.140s | 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.190s | 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.127s | passed |
| [7] seqEmpty.dl, seqLen(seqEmpty) = 0 | testSMTLemmaSoundness(String, String)[7] | 4.122s | 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.135s | 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.121s | passed |
Standard output
940191 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 940191 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 940191 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 940207 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 944286 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 944301 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jmod.dl.proof 944301 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.28ms 944419 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4855128267584068558.key 944419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSub.dl_4855128267584068558.key 944419 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.5ns 944419 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 948476 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 948492 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl_4855128267584068558.key 948492 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 948601 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 948601 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 948601 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.1ns 948601 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 952694 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.09s 952709 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqGetOutside.dl.proof 952756 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.38ms 952866 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2284313760397489171.key 952866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_singleton.dl_2284313760397489171.key 952866 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 212ns 952866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 956878 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 956893 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_singleton.dl_2284313760397489171.key 956893 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 957006 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17628311820684789478.key 957006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_create.dl_17628311820684789478.key 957006 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 467.1ns 957006 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 961055 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.06s 961070 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_create.dl_17628311820684789478.key 961086 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 961196 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_18027756872308518608.key 961196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allFields.dl_18027756872308518608.key 961196 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.8ns 961196 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 965194 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 965210 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allFields.dl_18027756872308518608.key 965210 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.1ns 965323 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7006428120835660991.key 965323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqEmpty.dl_7006428120835660991.key 965323 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.9ns 965323 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 969319 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 969319 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqEmpty.dl_7006428120835660991.key 969335 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.2ns 969445 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9754257695257387521.key 969445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_union.dl_9754257695257387521.key 969445 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 227ns 969445 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 973452 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 973468 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_union.dl_9754257695257387521.key 973468 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 973580 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_2645233277686453415.key 973580 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_2645233277686453415.key 973580 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.5ns 973580 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 977569 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 977585 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl.2_2645233277686453415.key 977585 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 977701 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10946382376078412785.key 977701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_wellFormed.dl_10946382376078412785.key 977701 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.6ns 977701 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 981704 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 981719 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_wellFormed.dl_10946382376078412785.key 981719 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 981845 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 981845 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 981845 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 981845 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 985830 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 985846 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_jdiv.dl.proof 985846 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.9ns 985955 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15110406681614995520.key 985955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_empty.dl_15110406681614995520.key 985955 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.4ns 985955 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 989950 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 989966 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_empty.dl_15110406681614995520.key 989966 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 990082 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10544244888683439869.key 990082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_allLocs.dl_10544244888683439869.key 990082 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 990082 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 994079 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 994094 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_allLocs.dl_10544244888683439869.key 994094 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.7ns 994211 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15435292857349194403.key 994211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_arrayRange.dl_15435292857349194403.key 994211 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.3ns 994211 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 998246 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 998261 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_arrayRange.dl_15435292857349194403.key 998261 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 998371 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3166937588490202038.key 998371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqConcat.dl_3166937588490202038.key 998371 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns 998371 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1002384 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 1002400 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqConcat.dl_3166937588490202038.key 1002400 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1002504 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14558768231829433356.key 1002504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqLen.dl_14558768231829433356.key 1002504 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.6ns 1002504 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1006542 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1006558 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqLen.dl_14558768231829433356.key 1006558 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ns 1006674 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16450549014309158892.key 1006674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_length.dl_16450549014309158892.key 1006674 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.4ns 1006674 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1010692 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 1010707 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_length.dl_16450549014309158892.key 1010707 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.6ns 1010822 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2974405590991790377.key 1010822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_freshLocs.dl_2974405590991790377.key 1010822 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.1ns 1010822 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1014841 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 1014857 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_freshLocs.dl_2974405590991790377.key 1014857 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ns 1014971 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17170426062778038030.key 1014971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_anon.dl_17170426062778038030.key 1014971 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.3ns 1014971 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1019026 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 1019042 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_anon.dl_17170426062778038030.key 1019042 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 1019152 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11753786038439674855.key 1019152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_memset.dl_11753786038439674855.key 1019152 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.3ns 1019152 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1023164 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 1023180 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_memset.dl_11753786038439674855.key 1023180 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 1023289 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14130273394520948811.key 1023289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_store.dl_14130273394520948811.key 1023289 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.7ns 1023289 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1027331 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 1027347 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_store.dl_14130273394520948811.key 1027347 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 1027456 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_825769546043126443.key 1027456 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_825769546043126443.key 1027456 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.6ns 1027456 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1031474 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 1031490 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSub.dl.2_825769546043126443.key 1031490 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1031600 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3926033264035895795.key 1031600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_seqSingleton.dl_3926033264035895795.key 1031600 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.6ns 1031600 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1035667 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1035683 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl_3926033264035895795.key 1035683 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 1035796 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_15959692171089041070.key 1035796 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_15959692171089041070.key 1035796 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 1035796 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1039855 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 1039870 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_seqSingleton.dl.2_15959692171089041070.key 1039870 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 1039995 INFO Test worker d.u.i.k.s.n.ProveSMTLemmasTest Now processing file C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10609562387542753569.key 1039995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\SMT_lemma_null.dl_10609562387542753569.key 1039995 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.9ns 1039995 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 1044003 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 1044018 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof SMT_lemma_null.dl_10609562387542753569.key 1044018 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns