TestLocalSymbols

2

tests

0

failures

0

ignored

8.214s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 8.173s passed
testSkolemization() 0.041s passed

Standard output

147759     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
147760     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
147763     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147764     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147764     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
147765     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147766     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147774     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
147775     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
147776     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147777     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
147778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147779     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
147802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
147808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.5ns 
147809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
148273     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
148275     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
148275     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
150191     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
155674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.87s 
155735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
155819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35ns 
155910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
155936     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'' 
155946     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''