Bad file formatting causes segmentation fault

[AntonXue]

Modified 172.smt2 file from the website example with the first line commented out:

; (set-logic QF_NRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(assert (<= 3.0 x1))
(assert (<= x1 3.14))
(assert (<= -7.0 x2))
(assert (<= x2 5.0))
(assert (<= (- (* 2.0 3.14159265) (* 2.0 (* x1 (arcsin (* (cos 0.797) (sin (/ 3.14159265 x1)))))))
            (+ (- 0.591 (* 0.0331 x2)) (+ 0.506 1.0))))
(check-sat)
(exit)

Crashes with the following message when run with only --verbose flag:

# OpenSMTContext::Declaring function x1 of sort () Real
# OpenSMTContext::Declaring function x2 of sort () Real
Segmentation fault

Proposed solution: make file format compliance user's job.

[soonho-tri]

Sorry for the delay in response. This is a known issue. In OpenSMT, it's harder to fix than it looks. The new version will take care of this issue.

[DustinWehr]

It'd be very helpful if this was mentioned in the readme.