smt

44 Questions
Newest Active Unanswered Frequent
Score
View
Card Compact
Without unwinding, translate a simple while loop iteration into SMT-LIB formula to prove correctness
user_10377290
•
2
1
64
smt verification z3py z3 while-loop
What does it mean for a fact used in Isabelle to have a number after the name?
user_131308340
•
2
1
42
hol smt isabelle z3
Evaluating assigned variables and clauses in Z3?
user_28821250
•
1
1
35
smt z3py z3 python
How to use z3-solver using threading module in python?
user_96667130
•
1
1
71
smt z3 python-3.x multithreading python
Using SBV to show satisfiability of predicates containing byte strings in Haskell
user_38774030
•
2
1
90
smt sbv bytestring haskell
Inductive proofs in theorem provers (Z3, Vampire, with TPTP syntax)
user_133125800
•
1
2
158
theorem-proving smt z3 logic-programming logic
Modelling finite field arithmetic mod p in Z3
user_175245960
•
1
0
69
finite-field smt z3 formal-verification
When will the SMT-LIB standard be extended to include optimization?
user_102643220
•
1
1
42
smt z3
z3 returning unknown when using Floats and Reals together?
user_146934600
•
1
1
42
smt z3
Can the mkOr(Expr<BoolSort> ... t) fuction in the Z3 Java Api get a list as input?
user_86271800
•
2
1
49
smt z3 solver java
Hot Questions