SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

Doesn't always exit immediately on error #415

Open stevenmeker opened 1 year ago

stevenmeker commented 1 year ago

Yices claims to implement the immediate-exit alternative for handling errors but doesn't always exit after reporting an error:

./yices_smt2 --version Yices 2.6.4 Copyright SRI International. Linked with GMP 6.2.0 Copyright Free Software Foundation, Inc. Build date: 2022-11-03 Platform: x86_64-pc-linux-gnu (release) Revision: unknown

(get-info :error-behavior) (:error-behavior immediate-exit) (declare-sort foo 0) (error "no logic set") (get-info :error-behavior) (:error-behavior immediate-exit)