TestLocalSymbols

2

tests

0

failures

0

ignored

7.203s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 7.148s passed
testSkolemization() 0.055s passed

Standard output

129645     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
129646     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
129657     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129658     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129659     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
129659     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129660     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129667     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
129668     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
129668     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129669     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129669     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
129670     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129670     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
129686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
129692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.4ns 
129692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130086     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
130088     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
130089     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
130089     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131565     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
136487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.79s 
136549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
136639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.1ns 
136758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
136800     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'' 
136806     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''