TestLocalSymbols

2

tests

0

failures

0

ignored

9.312s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 9.252s passed
testSkolemization() 0.060s passed

Standard output

153744     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
153744     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
153760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
153775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
153775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
153807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
153807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 964.4ns 
153822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154359     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
154359     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
154374     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
154374     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
156563     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
162590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.75s 
162684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
162810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.3ns 
162935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
162997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
163013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''