mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-03 08:38:06 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-11-01 13:06:16 -07:00
commit 4f2b7049ab
187 changed files with 493 additions and 33625 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/pdr_context.cpp
View file

@ -1325,7 +1325,7 @@ namespace pdr {
for (; it != end; ++it) {
ptr_vector<datalog::rule> const& rules = it->m_value->rules();
for (unsigned i = 0; i < rules.size(); ++i) {
datalog::rule* rule = rules[i];
// datalog::rule* rule = rules[i];
// vs(rule->get_head(),
// apply interpretation of predicates to rule.
// create formula and check for unsat.