diff --git a/z3.go b/z3.go
index b202ff2..3000175 100644
--- a/z3.go
+++ b/z3.go
@@ -12,7 +12,7 @@
 package z3
 
 // #cgo CFLAGS: -Ivendor/z3/src/api
-// #cgo LDFLAGS: ${SRCDIR}/libz3.a -lstdc++
+// #cgo LDFLAGS: ${SRCDIR}/libz3.a -lstdc++ -lm
 // #include <stdlib.h>
 // #include "go-z3.h"
 import "C"
diff --git a/z3_examples_test.go b/z3_examples_test.go
index 3870200..d2a1fa1 100644
--- a/z3_examples_test.go
+++ b/z3_examples_test.go
@@ -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)
@@ -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
 }