TestLocalSymbols

2

tests

0

failures

0

ignored

6.470s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.421s passed
testSkolemization() 0.049s passed

Standard output

120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120365     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120380     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
120427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 656.8ns 
120427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120818     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120818     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120818     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120818     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
122054     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
126525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.08s 
126572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
126682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.5ns 
126760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
126791     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'' 
126807     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''