YICES-SMT2(1)

📦 version 2.7.0, in fedora 43, fedora 44

💖 NAME 💖

yices-smt2 — the Yices SMT solver for the SMT-LIB 2 language. yes bestie, that's the whole vibe: a solver, and it speaks SMT-LIB 2 🌸

✨ SYNOPSIS ✨

yices-smt2 [ option ] [ file ]

🦋 DESCRIPTION 🦋

So basically yices-smt2 runs the Yices SMT solver on an input problem that's written in the SMT-LIB 2 language. If you don't hand it a file, it just reads the problem from standard input. no file? no problem. she'll take it from stdin, iconic behavior 💅

The SMT-LIB language and its logical theories are documented over at http://smtlib.cs.uiowa.edu — go read, it's giving homework but make it math 🧚

🎀 OPTIONS 🎀

  • --version, -V — Display version and exit. quick lil "who am I" moment and then she's gone 👋
  • --help, -h — Display a short help summary.
  • --verbosity=level, -v level — Set the verbosity level (default = 0). chattier with higher levels, silent-ish at zero 🤫
  • --timeout=timeout, -t timeout — Give a timeout in seconds. There is no timeout by default — she will simply keep going, forever, no cap 😭
  • --stats, -s — Print a statistics summary before exiting. receipts, basically 📊
  • --incremental — Enable support for the push/pop commands. you know, the stack era of your solving life 🫶
  • --interactive — Run in interactive mode.
    • This option is ignored if an input file is given on the command line. Otherwise, yices-smt2 prints a prompt before every command. This also sets the SMT-LIB option :print-success to true. so you get a lil prompt bestie, and every command says it worked 💬
  • --mcsat — Force use of the MCSAT solver. not asking, forcing 👑
  • --yices-model-format — Print models in the Yices model format (instead of the SMT-LIB format).. (yes the double period is canon, we respect the source 🙈)
  • --bvconst-in-decimal — Print bitvector constants using the SMT-LIB decimal format, instead of the binary format. decimal girlies rise 🌈
  • --delegate=solver — Selects an third-party backend SAT solver for bit-vector problems.
    • The solver must be either cadical or cryptominisat or y2sat. those are the only three, don't get cute 💀
    • This option has no effect unless the logic if QF_BV.
  • --dimacs=filename — Bit-blast then export the CNF to a file in the DIMACS format. This option is ignored unless the logic is QF_BV. bit-blasting is so extra and I love it ⚡
  • --mcsat-help — Display options used only by the MCSAT solver. the MCSAT-exclusive lore 🔥

👀 SEE ALSO 👀

To report bugs and to get the full documentation, please visit http://yices.csl.sri.com. found a bug? tell the internet, she's listening 🐛

💜 AUTHORS 💜

Copyright (C) SRI International. periodt ✨

Yices is developed at SRI's Computer Science Laboratory. The main developers are Bruno Dutertre <bruno@csl.sri.com>, Dejan Jovanovic <dejan@csl.sri.com>, Ian A. Mason <iam@csl.sri.com>, and Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>. absolute legends, all of them 👑👑👑👑

okay that's the whole page, mwah 💋 this was Yices 2.7.0, dated July 2025, and it lives at YICES-SMT2(1) — go solve something gorgeous, bestie 🦋💖

📦 where this page comes from