Fx 7 or In Software , It Is All About Quantifiers

Fx7 is an SMT solver for first order formulas, built over linear arithmetic and uninterpreted function symbols. Fx7 is implemented in the Nemerle language and runs on the .NET platform, specifically the solver was developed and tested using Mono, an open source .NET implementation. Fx7 is available under a BSD-like license from http://nemerle.org/fx7/. It was designed for software verification queries, like the ones generated by ESC/Java [6] and Boogie [1] tools. These queries do not put much pressure on arithmetic, instead they make heavy use of quantifiers in axiomatization of the checked programming language semantics. Fx7 is therefore mainly a research vehicle for testing different strategies of dealing with quantifiers. We want to compete only in the AUFLIA division and expect to do well in terms of number of benchmarks solved and not-so-well in terms of total time taken. Our answer to the random seed question is (obviously) 42. “SAT” Answer: During the competition the solver will never say the formula is satisfiable. This is due to inherent incompleteness of quantifier instantiation and high penalty for giving wrong answer. On the other hand, in the “real world” applications we have found it very important to answer promptly that the formula is satisfiable with some degree of confidence. We feel that the next SMT competition should somehow accommodate for this fact in the scoring rules.