Skip to content
This repository has been archived by the owner on Oct 31, 2023. It is now read-only.

Commit

Permalink
Merge pull request #4 from mattn/fix-build
Browse files Browse the repository at this point in the history
Fix build
  • Loading branch information
mitchellh authored Dec 28, 2019
2 parents 2c27925 + 857a8e1 commit 4cbedeb
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 5 deletions.
2 changes: 1 addition & 1 deletion error.go
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ func (c *Context) SetErrorHandler(f ErrorHandler) {
//
// Maps: Z3_get_error_msg_ex
func (c *Context) Error(code ErrorCode) string {
return C.GoString(C.Z3_get_error_msg_ex(c.raw, C.Z3_error_code(code)))
return C.GoString(C.Z3_get_error_msg(c.raw, C.Z3_error_code(code)))
}

//export goZ3ErrorHandler
Expand Down
8 changes: 7 additions & 1 deletion model.go
Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
package z3

// #include "go-z3.h"
/*
int _Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, int model_completion, Z3_ast * v) {
return Z3_model_eval(c, m, t, (bool) model_completion, v);
}
*/
import "C"

// Model represents a model from a solver.
Expand Down Expand Up @@ -34,7 +40,7 @@ func (m *Model) String() string {
// Maps: Z3_model_eval
func (m *Model) Eval(c *AST) *AST {
var result C.Z3_ast
if C.Z3_model_eval(m.rawCtx, m.rawModel, c.rawAST, C.Z3_TRUE, &result) != C.Z3_TRUE {
if C._Z3_model_eval(m.rawCtx, m.rawModel, c.rawAST, 1, &result) == 0 {
return nil
}

Expand Down
4 changes: 2 additions & 2 deletions model_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ func TestModelAssignments(t *testing.T) {
// Solve
result := s.Check()
if result != True {
t.Fatalf("bad: %s", result)
t.Fatalf("bad: %v", result)
}

// Get the model
Expand Down Expand Up @@ -71,7 +71,7 @@ func TestModelEval(t *testing.T) {
// Solve
result := s.Check()
if result != True {
t.Fatalf("bad: %s", result)
t.Fatalf("bad: %v", result)
}

// Get the model
Expand Down
2 changes: 1 addition & 1 deletion solver_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ func TestSolver(t *testing.T) {
// Solve
result := s.Check()
if result != True {
t.Fatalf("bad: %s", result)
t.Fatalf("bad: %v", result)
}

// Get the model
Expand Down

0 comments on commit 4cbedeb

Please sign in to comment.