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

[rainoftime]

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]

Thanks for reporting this. I can reproduce the issue.