YICES-SMT(1)

📦 version 2.7.0, in fedora 43, fedora 44

✨ yices-smt — the Yices SMT solver, but make it SMT-LIB 1.2 💅

okay bestie, so this is yices-smt, and she's the Yices SMT solver for the SMT-LIB 1.2 language. yes, she's a whole icon. 🎀

🌸 NAME 🌸

yices-smt — the Yices SMT solver for the SMT-LIB 1.2 language 🦋

🎀 SYNOPSIS 🎀

yices-smt [ options ] [ file ]

✨ DESCRIPTION ✨

So basically, this runs the Yices SMT solver on an input problem that's written in SMT-LIB 1.2. Simple as that. 💖

And if you don't hand her a file? No worries, she just reads the problem straight from standard input. main character energy, she comes to you. 😌

okay ngl, a little lore drop: SMT-LIB 1.2 is the old version of the SMT-LIB language. It got replaced by SMT-LIB 2.0 back in 2012. so yeah, she's vintage. nostalgic. we love her anyway. 🫶

💅 OPTIONS 💅

  • --version, -V — shows you the version and then dips. that's it, that's the whole job. ✨
  • --help, -h — prints a short help summary for when you're lost (no shame, we've all been there). 🦋
  • --model, -m — if the problem is satisfiable, she prints a model to stdout. heads up tho: some variables may be eliminated. it's giving "here's the vibe, not every detail." 💖
  • --full-model, -f — if the problem is satisfiable, she prints a full model. and fr fr, this one gives you more details than --model does. the deluxe edition, no cap. 👑
  • --verbose, -v — prints statistics and other data during the search. she's narrating the whole journey. 🗣️
  • --stats, -s — prints a statistics summary at the end of the search. the wrap-up. the outro. the credits. 🎬
  • --timeout=timeout, -t timeout — gives her a timeout in seconds. and listen: by default there is no timeout at all. she will simply keep going. forever. bestie has no concept of stopping. 😭

🦋 SEE ALSO 🦋

And for bug reporting + other info, please visit http://yices.csl.sri.com. go say hi, they're lovely. 💖

👑 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>
  • Stephane Graham-Lengrand <stephane.graham-lengrand@sri.com>

Yices 2.7.0 · July 2025 — and that's the whole page bestie, ty for coming to my TED talk, mwah 💅✨🌸🦋🎀💖👑🫶

📦 where this page comes from