axiom-profiler icon indicating copy to clipboard operation
axiom-profiler copied to clipboard

Published 20 hours ago • verified publisher icon viperproject

Missing instantiation of inner/nested quantifier

Open mschwerhoff opened this issue 4 years ago • 0 comments

Note: Reducing attached SMT file to its minimum revealed issue #26.

Running SMT file set_equals_triggers_datatypes.smt2.txt on Z3 4.8.6 on Windows 10 produced z3.log. Loading this into the axiom profiler shows an instantiation of axiom Set_equal_outer, and instantiations of datatype axioms that are triggered by terms that — I believe — have been obtained from instantiating axiom Set_equal_inner. According to the profiler, however, the latter was not instantiated.

mschwerhoff avatar May 26 '20 13:05 mschwerhoff