TestLocalSymbols

2

tests

0

failures

0

ignored

9.393s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 9.297s passed
testSkolemization() 0.096s passed

Standard output

149143     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
149155     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
149164     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149166     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149169     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
149170     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149171     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149188     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
149189     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
149196     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149198     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149198     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
149199     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149200     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
149220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
149231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.6ms 
149234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149781     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
149783     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
149785     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
149786     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
152398     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
158078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.84s 
158212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
158345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.9ns 
158438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
158478     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'' 
158486     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''