YICES(1)

📦 version 2.7.0, in fedora 43, fedora 44

👑 NAME 👑

yices — the Yices SMT solver, but make it for the Yices language 💅

okay bestie, quick vibe check: this is the Yices SMT solver page from the User Commands manual. It's giving "I solve your satisfiability problems and I look cute doing it." Periodt.

✨ SYNOPSIS ✨

yices [ options ] [ file ]

🦋 DESCRIPTION 🦋

So basically it runs the Yices SMT solver. The way this works is: your input has to be in the Yices specification language — no cap, that's the only language it speaks, it's not bilingual bestie.

And if you don't hand it a file? No problem. Yices just reads commands straight from standard input. She's flexible like that. 🫶

💖 OPTIONS 💖

  • --version, -V — shows you the version and then dips. That's it, that's the whole job. ✨
  • --help, -h — gives you a short lil help summary so you're not out here lost.
  • --verbosity=level, -v level — sets the verbosity level. The default is 0, so if you want more chatter you gotta ask for it. 🗣️
  • --logic=name — configures Yices for a specific logic.

The name has to be either an SMT-LIB logic name (like QF_UFLIA, iykyk) or the special symbol NONE if you wanna select propositional logic.

  • --arith-solver=solver — picks the arithmetic solver.

The solver can be simplex or floyd-warshall or auto. Heads up though: this option gets ignored unless the logic is either QF_RDL or QF_IDL. So don't come crying if you set it and nothing happens. 😭

  • --mode=mode — selects the usage mode.

The mode can be one-shot or multi-checks or interactive or push-pop or ef. Let's break it down:

  • one-shot: only one call to (check) is allowed. No assertions after (check), okay? And the commands (push) and (pop) are not supported. One and done, main character energy. 👑
  • multi-checks: several calls to (check) are allowed. You can add assertions after a check. But (push) and (pop)? Still not supported. 🙈
  • push-pop: like multi-check but now with support for (push) and (pop). Glow up. ✨
  • interactive: like push-pop. On top of that, Yices restores the context to a clean state if (check) gets interrupted. Very self-care of her. 🌸
  • ef: enables the exist-forall solver, meaning the command (ef-solve) can be used. This one's like one-shot in that only one call to (ef-solve) is allowed.

The default mode is push-pop. 💅

  • --mcsat — forces use of the MCSAT solver. Just force it. Be assertive. 🔥
  • --print-success — prints ok after every command that would otherwise execute silently. So now you get the lil receipt for everything. 🎀

🌈 SEE ALSO 🌈

yices-sat(1), yices-smt(1), yices-smt2(1)

Wanna report bugs or get the full documentation? Bestie, please visit http://yices.csl.sri.com. They got you. 🫶

💜 AUTHORS 💜

Copyright (C) SRI International.

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 icons, every single one. 👑

k that's the whole page bestie, no notes. This was Yices 2.7.0, from July 2025, and the manual is YICES(1) — slay, bye! 💖✨🦋

📦 where this page comes from