Fix build and a failing test

[mholtom]

The latest version of z3 would fail to run the tests when built:

go test -v
# github.com/mitchellh/go-z3
/usr/bin/ld: ./libz3.a(hwf.o): undefined reference to symbol 'remainder@@GLIBC_2.2.5'
/usr/bin/ld: /lib/x86_64-linux-gnu/libm.so.6: error adding symbols: DSO missing from command line
collect2: error: ld returned 1 exit status
FAIL    github.com/mitchellh/go-z3 [build failed]

I have added a reference to the Math library with -lm to fix this problem.

When the tests built after applying the fix, there was a failing test:

=== RUN   ExampleFindModel2
--- FAIL: ExampleFindModel2 (0.01s)
got:
Solving part 1
x = 0
y = 1

Solving part 2
x = (- 1)
y = 0
want:
Solving part 1
x = 0
y = 1

Solving part 2
x = 0
y = 1
FAIL

Which I fixed to match the comment.

go-z3/z3_examples_test.go

Line 137 in 4cbedeb

// x < y + 1 && x > 2

Also with the additional constraint:

go-z3/z3_examples_test.go

Line 163 in 4cbedeb

// !(x == y)

Giving a new output:

go-z3/z3_examples_test.go

Lines 183 to 190 in 121f7c6

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

[raulojeda22]

This commit solved my issue, thanks 👍

[shenyimings]

Thank you very much! This solved my issue, and using the MAKEFILE you provided reduced the previously lengthy build time.