TestLocalSymbols

2

tests

0

failures

0

ignored

6.203s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.165s passed
testSkolemization() 0.038s passed

Standard output

93588      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93603      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93619      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
93619      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93619      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
93652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
93660      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.55ms 
93660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93977      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
93977      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
93977      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
93977      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
95380      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
98998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 
99060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
99123      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.2ns 
99263      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
99763      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
99763      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''