diff --git a/src/api/go/fixedpoint.go b/src/api/go/fixedpoint.go index 7ed94c542..ab28569fc 100644 --- a/src/api/go/fixedpoint.go +++ b/src/api/go/fixedpoint.go @@ -81,7 +81,7 @@ func (f *Fixedpoint) AddFact(pred *FuncDecl, args []int) { C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, 0, nil) return } - + cArgs := make([]C.uint, len(args)) for i, arg := range args { cArgs[i] = C.uint(arg) @@ -109,12 +109,12 @@ func (f *Fixedpoint) QueryRelations(relations []*FuncDecl) Status { if len(relations) == 0 { return Unknown } - + cRelations := make([]C.Z3_func_decl, len(relations)) for i, rel := range relations { cRelations[i] = rel.ptr } - + result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0]) switch result { case C.Z3_L_TRUE: @@ -253,12 +253,12 @@ func (s *Statistics) GetKey(idx int) string { // IsUint returns true if the statistical data at the given index is unsigned integer func (s *Statistics) IsUint(idx int) bool { - return bool(C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx))) + return bool(C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx))) } // IsDouble returns true if the statistical data at the given index is double func (s *Statistics) IsDouble(idx int) bool { - return bool(C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx))) + return bool(C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx))) } // GetUintValue returns the unsigned integer value at the given index diff --git a/src/api/go/z3.go b/src/api/go/z3.go index be74829d5..3e11dadf6 100644 --- a/src/api/go/z3.go +++ b/src/api/go/z3.go @@ -547,12 +547,12 @@ return newExpr(q.ctx, q.ptr) // IsUniversal returns true if this is a universal quantifier (forall) func (q *Quantifier) IsUniversal() bool { -return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr)) +return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr)) } // IsExistential returns true if this is an existential quantifier (exists) func (q *Quantifier) IsExistential() bool { -return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr)) +return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr)) } // GetWeight returns the weight of the quantifier