TestLocalSymbols

2

tests

0

failures

0

ignored

8.306s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 8.237s passed
testSkolemization() 0.069s passed

Standard output

152795     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
152797     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
152803     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152804     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152805     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
152808     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152816     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152824     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
152825     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
152827     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152830     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152831     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
152833     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152834     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
152855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
152870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
152879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153390     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
153392     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
153402     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
153403     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
154957     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
160740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.86s 
160816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
160937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.5ns 
161038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
161063     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'' 
161067     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''