mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity

Fix trailing whitespace in Go source files

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 06:06:48 +00:00
parent 3f4bd11f00
commit d33c0e5601
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/go/fixedpoint.go
View file

@ -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

4
src/api/go/z3.go
View file

@ -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