Discussions

• 1 You must be logged in to vote

  🙏

  set.filter behavior/performance

  cgjohannsen asked May 31, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Multiple synth-fun sharing the same grammar

  zhengyao-lin asked May 25, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Unsat core when sygus returns infeasible

  zhengyao-lin asked May 24, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Mapping over arrays?

  clayrat asked May 23, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Solver answering with unevaluated expression

  pfroehle-ccl asked May 16, 2024 in Q&A · Unanswered

  

  

  

  

  3
• 1 You must be logged in to vote

  💡

  Support for rem to match z3

  yav started May 16, 2024 in Ideas

  

  

  1
• 1 You must be logged in to vote

  🙏

  How to create a floating point term from a floating point

  thealberto asked May 12, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  How to track code coverage of cvc5 using --coverage and gcovr command

  YuanchengJiang asked Apr 30, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Quantifiers with recursive datatypes causes 'incomplete'

  aidanhs asked May 10, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  [Question]: How to install python3 cvc5 base api with --python-bindings?

  hagozaebii asked Dec 27, 2023 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  SyGuS vs. Rosette performance

  jefftrull asked Apr 3, 2024 in Q&A · Unanswered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Parsing a formula using C++/Python API

  pkalita595 asked Sep 3, 2022 in Q&A · Answered

  

  

  

  

  4
• 1 You must be logged in to vote

  💡

  Use compiler optimizations to simplify VC in specific theories

  yannickmoy started Apr 12, 2024 in Ideas

  

  

  0
• 1 You must be logged in to vote

  🙏

  Adding Macros to a SyGuS Grammar

  NeumannDirk asked Mar 18, 2024 in Q&A · Unanswered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Time and Resource Limits for Synthesis

  NeumannDirk asked Apr 10, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  The question about an error when test the example of the Theory of Finite Fields.

  valeryjust asked Feb 26, 2024 in Q&A · Answered

  

  

  

  

  3
• 1 You must be logged in to vote

  🙏

  Does cvc5 have a way to understand an SMTLIB string with its Python api? (Something like Z3's .from_string())

  TiloRC asked Apr 7, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Adding support for Z3's fp.to_ieee_bv (or workaround?)

  bavalpey asked Nov 17, 2022 in Q&A · Unanswered

  

  

  5
• 1 You must be logged in to vote

  🙏

  Reduction of assumptions in (get-unsat-assumptions)

  grhcj asked Apr 4, 2024 in Q&A · Closed · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💬

  Linux aarch64 build?

  robby-phd started Dec 7, 2023 in General

  

  

  2
• 1 You must be logged in to vote

  🙏

  Read a SMT-LIB2 file and solve it for all solutions in C++

  lenchil asked Mar 4, 2024 in Q&A · Unanswered

  

  

  3
• 1 You must be logged in to vote

  🙏

  Segfault with Proof Generation

  fslivovsky asked Mar 22, 2024 in Q&A · Answered

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  Quadratic/cubic performance with additional assertions about defined recursive function

  jbosboom asked Mar 26, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Some questions about --minisat-dump-dimacs.

  TraceShadow asked Mar 26, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💬

  Multiple-threaded synthesis

  lvtao-sec started Mar 10, 2024 in General

  

  

  3