search

SRI-CSL / yices2

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

Displaying solving results when using --dimacs on trivial sat/unsat formulas #432

Open rainoftime opened 1 year ago

rainoftime commented 1 year ago

Hi, I tried running yices-smt2 --dimacs=tmp.cnf test.smt2 on the following trivial formula

(set-logic QF_BV)
(declare-fun x () (_ BitVec 16))
(assert (= x (_ bv1 16)))
(assert (= x (_ bv2 16)))
(check-sat)

Yices does not generate the tmp.cnf file and does not show anything on the screen. Perhaps it is because the formula has already been solved by the word-level preprocessing.

Maybe displaying "sat"/"unsat" result on the screen would be better?

My Yices version is 

 % yices-smt2 --version
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2023-03-14
Platform: arm-apple-darwin21.6.0 (release)
Revision: unknown
ahmed-irfan commented 1 year ago

Thanks for reporting this. I can reproduce the issue.