Reserved keyword 'min' in *.smt files

[Baranowski]

It seems that Z3's SMT2.0 parser treats 'min' as a builtin symbol and so cannot process files created by hcc.

For example when I run:
z3 -smt2 -nw Simple.unjuggle_not.smt

I get:
(error "line 3 column 25: invalid declaration, builtin symbol min")
(error "line 13 column 41: invalid number of arguments to floating point operator")
(error "line 16 column 35: invalid number of arguments to floating point operator")
(error "line 18 column 35: invalid number of arguments to floating point operator")
(error "line 20 column 34: invalid number of arguments to floating point operator")
(error "line 22 column 34: invalid number of arguments to floating point operator")
(error "line 32 column 57: invalid number of arguments to floating point operator")
(error "line 34 column 46: invalid number of arguments to floating point operator")
(error "line 36 column 48: invalid number of arguments to floating point operator")
(error "line 38 column 47: invalid number of arguments to floating point operator")
(error "line 41 column 62: invalid number of arguments to floating point operator")
(error "line 53 column 36: invalid number of arguments to floating point operator")
(error "line 56 column 37: invalid number of arguments to floating point operator")
(error "line 57 column 35: invalid number of arguments to floating point operator")
(error "line 61 column 30: invalid number of arguments to floating point operator")
(error "line 62 column 30: invalid number of arguments to floating point operator")
(error "line 66 column 43: invalid number of arguments to floating point operator")
(error "line 67 column 56: invalid number of arguments to floating point operator")

I'm using Z3 v. 4.3.1.

I've created a quick fix at Baranowski@98addaf. Not making a pull request since there is probably a better way to deal with it.

[danr]

The place to go is halo/src/Halo/FOL/LineariseSMT.hs, and change linMin :: SDoc.

I tried to fix it but I've forgot how to deal with this submodule mess :)

I guess the right thing would be to subtree merge halo into this directory since noone else depends on it stand alone anymore. HipSpec used to, but it has a new Haskell -> Logic translation.