mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-03-24 11:26:07 -07:00
commit ee5d61bd60
3 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -11,7 +11,7 @@ Abstract:
The linear invariants are extracted according to Karr's method.
A short description is in
Nikolaj Bjørner, Anca Browne and Zohar Manna. Automatic Generation
Nikolaj Bjorner, Anca Browne and Zohar Manna. Automatic Generation
of Invariants and Intermediate Assertions, in CP 95.
The algorithm is here adapted to Horn clauses.

6
src/muz_qe/hnf.cpp
View file

@ -353,7 +353,8 @@ private:
void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) {
for (unsigned i = 0; i < body.size(); ++i) {
eliminate_disjunctions(body[i], proofs);
expr_ref_vector::element_ref r = body[i];
eliminate_disjunctions(r, proofs);
}
}
@ -378,7 +379,8 @@ private:
void eliminate_quantifier_body(expr_ref_vector& body, proof_ref_vector& proofs) {
for (unsigned i = 0; i < body.size(); ++i) {
eliminate_quantifier_body(body[i], proofs);
expr_ref_vector::element_ref r = body[i];
eliminate_quantifier_body(r, proofs);
}
}

2
src/util/bit_vector.cpp
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#include<limits.h>
#include"bit_vector.h"
#include"util.h"
#include"trace.h"