mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Fix gcc compilation errors

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-03-24 09:07:51 -07:00
parent 5aa84c28a6
commit 9d0b0df985
2 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/hnf.cpp
View file

@ -353,7 +353,8 @@ private:
void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) { void eliminate_disjunctions(expr_ref_vector& body, proof_ref_vector& proofs) {
for (unsigned i = 0; i < body.size(); ++i) { 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) { void eliminate_quantifier_body(expr_ref_vector& body, proof_ref_vector& proofs) {
for (unsigned i = 0; i < body.size(); ++i) { 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: Revision History:
--*/ --*/
#include<limits.h>
#include"bit_vector.h" #include"bit_vector.h"
#include"trace.h" #include"trace.h"