TestLocalSymbols

2

tests

0

failures

0

ignored

8.299s

duration

100%

successful

Tests

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

Standard output

156066     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
156068     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
156073     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156074     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156075     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
156076     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156077     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156082     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
156083     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
156084     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156088     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
156090     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156091     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
156113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
156134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.71ns 
156135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156667     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
156667     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
156671     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
156673     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
158228     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
164072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.94s 
164135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
164234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.8ns 
164309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
164328     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'' 
164332     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''