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

Commit 4cbedeb

Browse files
authored
Merge pull request #4 from mattn/fix-build
Fix build
2 parents 2c27925 + 857a8e1 commit 4cbedeb

File tree

4 files changed

+11
-5
lines changed

4 files changed

+11
-5
lines changed

error.go

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ func (c *Context) SetErrorHandler(f ErrorHandler) {
5050
//
5151
// Maps: Z3_get_error_msg_ex
5252
func (c *Context) Error(code ErrorCode) string {
53-
return C.GoString(C.Z3_get_error_msg_ex(c.raw, C.Z3_error_code(code)))
53+
return C.GoString(C.Z3_get_error_msg(c.raw, C.Z3_error_code(code)))
5454
}
5555

5656
//export goZ3ErrorHandler

model.go

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
11
package z3
22

33
// #include "go-z3.h"
4+
/*
5+
int _Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, int model_completion, Z3_ast * v) {
6+
return Z3_model_eval(c, m, t, (bool) model_completion, v);
7+
}
8+
9+
*/
410
import "C"
511

612
// Model represents a model from a solver.
@@ -34,7 +40,7 @@ func (m *Model) String() string {
3440
// Maps: Z3_model_eval
3541
func (m *Model) Eval(c *AST) *AST {
3642
var result C.Z3_ast
37-
if C.Z3_model_eval(m.rawCtx, m.rawModel, c.rawAST, C.Z3_TRUE, &result) != C.Z3_TRUE {
43+
if C._Z3_model_eval(m.rawCtx, m.rawModel, c.rawAST, 1, &result) == 0 {
3844
return nil
3945
}
4046

model_test.go

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ func TestModelAssignments(t *testing.T) {
2929
// Solve
3030
result := s.Check()
3131
if result != True {
32-
t.Fatalf("bad: %s", result)
32+
t.Fatalf("bad: %v", result)
3333
}
3434

3535
// Get the model
@@ -71,7 +71,7 @@ func TestModelEval(t *testing.T) {
7171
// Solve
7272
result := s.Check()
7373
if result != True {
74-
t.Fatalf("bad: %s", result)
74+
t.Fatalf("bad: %v", result)
7575
}
7676

7777
// Get the model

solver_test.go

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ func TestSolver(t *testing.T) {
2929
// Solve
3030
result := s.Check()
3131
if result != True {
32-
t.Fatalf("bad: %s", result)
32+
t.Fatalf("bad: %v", result)
3333
}
3434

3535
// Get the model

0 commit comments

Comments
 (0)