TestLocalSymbols

2

tests

0

failures

0

ignored

7.759s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 7.717s passed
testSkolemization() 0.042s passed

Standard output

145466     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
145467     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
145472     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145473     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145474     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
145475     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145476     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145482     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
145483     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
145484     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145485     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145486     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
145487     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145487     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
145505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
145511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 944.61ns 
145513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145941     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
145942     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
145944     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
145945     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
147666     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
152899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.39s 
152963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
153051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.4ns 
153144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
153187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 3, command: 'rule allRight formula='\forall int i; i > 0'' 
153192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 2, source line: 4, command: 'rule allRight formula='\forall int i; i < 0''