Discussions

• 1 You must be logged in to vote

  🙏

  Which lemmas are destroyed on pop?

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

  

  

  5
• 1 You must be logged in to vote

  🙏

  is there an implementation available in the high level api for string variables/sorts in typescript?

  uwesimm asked Jun 3, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Does z3 take and produce s-expressions?

  egel-lang asked May 27, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Need to call dec_ref after del_context?

  remysucre asked May 25, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  z3 py in overflow checking for bit-vectors

  hagozaebii asked Apr 19, 2024 in Q&A · Closed · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Tseitin Transformation with Z3 and final output Variable

  Flessent asked May 2, 2024 in Q&A · Answered

  

  

  6
• 1 You must be logged in to vote

  🙏

  Outermost existential quantifier prevents solution from being found

  pclayton asked Aug 30, 2023 in Q&A · Closed · Answered

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  Why is this result sat? I expected it to be unsat

  sengxin asked Apr 23, 2024 in Q&A · Closed · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Consistent speed-up of incremental solver (2) used in non-incremental way

  sreeshmaheshwar asked Apr 8, 2024 in Q&A · Answered

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  Detect Unsatisfiable Model in a Satisfiable Problem

  mfazelnia asked Mar 13, 2024 in Q&A · Unanswered

  

  

  7
• 1 You must be logged in to vote

  🙏

  Undetermined value in Z3?

  Muxucao0812 asked Apr 2, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Select one bit in BitVec

  Muxucao0812 asked Apr 1, 2024 in Q&A · Answered

  

  

  5
• 1 You must be logged in to vote

  🙏

  Want suggestion on improving performance using sequence solver

  smoy asked Mar 29, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  why first is SAT, but sencond is not SAT?

  willy3a asked Mar 24, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Can I use the Intermediate Data to accelerate solving speed?

  bobozi-cmd asked Mar 25, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  in Z3, constrains on a freedom array will not apply to another array, why?

  willy3a asked Mar 24, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Z3 prover: this Smtlib shoud not be SAT because last assert, why?

  willy3a asked Mar 23, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Understanding string solver performance in z3

  smoy asked Mar 21, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  How to introduce Z3 in Visual Studio

  xebelleDerrel asked Mar 21, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Running time and tactics for bounds on integer constraints

  mikekben asked Mar 12, 2024 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Building a rational AST using the C API

  turibe asked Mar 5, 2024 in Q&A · Unanswered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Retrieve function definition

  Axhinator asked Feb 27, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Unknown solution when multiplied by one

  anirjoshi asked Feb 16, 2024 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  User propagators vs. offline lemmas on demand, and clause deletion policies

  ThomasHaas asked Feb 2, 2024 in Q&A · Unanswered

  

  

  12
• 1 You must be logged in to vote

  🙏

  Question: how to build OCaml bindings on i686 where ocamlopt is no longer available?

  MIvanchev asked Feb 3, 2024 in Q&A · Unanswered

  

  

  1