search

viperproject / axiom-profiler

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
Other
32 stars 4 forks source link

Variable Names for Nested Quantifiers #4

Closed viper-admin closed 4 years ago

viper-admin commented 5 years ago

Created by bitbucket user nilsbecker_ on 2019-02-27 19:27 Last updated on 2019-04-26 15:15

Z3's internal indices are used to attach names and sorts to quantified variables. However, this does not work for nested quantifiers since z3 assigns the same indices to variables of the outer and inner quantifiers. E.g. in

#!smt2

forall x. A(x) && forall y. B(x, y)

both x and y are assigned index 0. Loading logs that contain nested quantifiers such as https://bitbucket.org/viperproject/axiom-profiler-test-logs/src/default/civl-example-from-siddharth/test-test_1.smt (also attached) usually raises exceptions which are caught by the fault tolerance mechanisms in release builds resulting in those variable names / sorts being ignored for that quantifier. In practice nested quantifiers are usually rewritten into a single quantifier before being instantiated so the user may not necessarily notice any issues.

Attachments:

viper-admin commented 5 years ago

Bitbucket user nilsbecker_ commented on 2019-04-26 15:15

This issue has been resolved with commit https://github.com/viperproject/axiom-profiler/commit/630465f1419349dd221bb863300cff3a313e354c.

viper-admin commented 5 years ago

Bitbucket user nilsbecker_ on 2019-04-26 15:15:

  • changed state from new to resolved