Skip to content

Commit

Permalink
🐛 fix bug according to a PR
Browse files Browse the repository at this point in the history
  • Loading branch information
Troublor committed Oct 17, 2021
1 parent 4cbedeb commit 7250353
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 8 deletions.
4 changes: 4 additions & 0 deletions go.mod
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module github.com/Troublor/go-z3

go 1.17

4 changes: 2 additions & 2 deletions z3.go
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@
// ErrorHandler and Context.SetErrorHandler for more information.
package z3

// #cgo CFLAGS: -Ivendor/z3/src/api
// #cgo LDFLAGS: ${SRCDIR}/libz3.a -lstdc++
// #cgo CFLAGS: -I ${SRCDIR}/lib/include
// #cgo LDFLAGS: ${SRCDIR}/lib/bin/libz3.a -lstdc++ -lm
// #include <stdlib.h>
// #include "go-z3.h"
import "C"
12 changes: 6 additions & 6 deletions z3_examples_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -128,8 +128,8 @@ func ExampleFindModel2() {
y := ctx.Const(ctx.Symbol("y"), ctx.IntSort())

// Create a couple integers
v1 := ctx.Const(ctx.SymbolInt(1), ctx.IntSort())
v2 := ctx.Const(ctx.SymbolInt(2), ctx.IntSort())
v1 := ctx.Int(1, ctx.IntSort())
v2 := ctx.Int(2, ctx.IntSort())

// y + 1
y_plus_one := y.Add(v1)
Expand Down Expand Up @@ -182,10 +182,10 @@ func ExampleFindModel2() {

// Output:
// Solving part 1
// x = 0
// y = 1
// x = 3
// y = 3
//
// Solving part 2
// x = 0
// y = 1
// x = 3
// y = 4
}

0 comments on commit 7250353

Please sign in to comment.