Discussions

• 1 You must be logged in to vote

  🙏

  Trying to understand reason for "unknown" because of "incomplete quantifiers"

  maggesi asked May 23, 2025 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  How to use solve_for

  philzook58 asked May 15, 2025 in Q&A · Answered

  

  

  2
• 1 You must be logged in to vote

  🙏

  z3 Array performance issues with large arrays

  Notselwyn asked Apr 26, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  How to disable the SIGINT signal handler?

  mikulas-patocka asked Mar 30, 2025 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  [Question] Is it possible to add randomness to generated solutions?

  jonathan-dilorenzo asked Mar 25, 2025 in Q&A · Unanswered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Performance difference when base address is fixed vs. symbolic in bitvector-based pointer analysis

  christophsanders asked Mar 18, 2025 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Puzzling "operator is applied to arguments of the wrong sort" with mkConcat in Java API

  yvanlabiche asked Feb 28, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💬

  Parametric type variables and Datatype parameters

  philzook58 started Feb 19, 2025 in General

  

  

  1
• 1 You must be logged in to vote

  🙏

  mkAllcharRe with compilation error

  yvanlabiche asked Feb 14, 2025 in Q&A · Unanswered

  

  

  1
• 2 You must be logged in to vote

  🙏

  Strange behaviour in the UserPropagate propagate function

  JoanEspasa asked Nov 26, 2024 in Q&A · Answered

  

  

  

  

  10
• 1 You must be logged in to vote

  🙏

  The runtime of z3 is too long

  frankeyjin asked Feb 3, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💬

  Parallel in z3 to speed up?

  XiangyuG started Jan 15, 2025 in General

  

  

  2
• 1 You must be logged in to vote

  🙏

  Solver params are ignored without push

  ole-thoeb asked Jan 14, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  How to reference sorts and functions imported from an SMT2 file/string in the C++ API?

  tschuchortdev asked Jan 1, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  💡

  TS/JS Bindings - Poor documentation, inconsistent API, ADTs?

  kizerkizer started Dec 18, 2024 in Ideas

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  [Question]: How can I get used lemmas about formula after solving?

  hagozaebii asked Dec 24, 2024 in Q&A · Unanswered

  

  

  0
• 2 You must be logged in to vote

  🙏

  Tseitin Rule in Proof Log

  HarryBryant99 asked Dec 20, 2024 in Q&A · Unanswered

  

  

  0
• 5 You must be logged in to vote

  💬

  rise4fun.com web page is down

  ftc started Aug 11, 2021 in General

  

  

  

  

  29
• 1 You must be logged in to vote

  🙏

  Give strictly greater value for x ≥ c

  leduyquang753 asked Nov 19, 2024 in Q&A · Unanswered

  

  

  1
• 3 You must be logged in to vote

  🙏

  Python: specifying "decide" in user propagator

  jordicollcaballero asked Oct 24, 2024 in Q&A · Unanswered

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  how to implementation “verify two functions equivalent example code with Z3 ” ？

  pily1 asked Nov 22, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Am I using Z3Py correctly? I'm concerned at how similar the proofs look

  LivInTheLookingGlass asked Nov 12, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  migration from yices to Z3

  fclaudel asked Oct 25, 2024 in Q&A · Unanswered

  

  

  2
• 1 You must be logged in to vote

  💬

  Supplementary z3 simplification projects

  Notselwyn started Nov 2, 2024 in General

  

  

  1
• 1 You must be logged in to vote

  🙏

  User Propagator: Register fixed only when value is True

  lukerooney7 asked Oct 21, 2024 in Q&A · Unanswered

  

  

  

  

  2