StackRating

An Elo-based rating system for Stack Overflow
Home   |   About   |   Stats and Analysis   |   Get a Badge
Rating Stats for

alias

Rating
1531.30 (17,435th) 		Reputation
8,170 (19,274th)
Page: 1 ... 11 12 13 14
Title Δ
Interaction between quantifiers and sets in z3 0.00
How can I tell Z3 where to start when solving a formula? 0.00
Why is Z3 having trouble using evenness information under some cond... 0.00
Declare matrix with unknown size in Z3 +0.33
Adding assertions to Z3 after loading in smt2 file with C++ API 0.00
Are equations with products of uninterpreted functions unsolvable i... 0.00
Is there an UnsignedIntSort in Z3? +0.16
How to use Z3 C++ API to prove a theory based on input parameter? 0.00
Z3 getting last valid model -3.71
Reduce the time for multiple modles 0.00
Not Solvable in Z3. Why? 0.00
Right set of tactics to use in Z3 to solve these inequalities 0.00
Why are Float and Double different in the case of adding 0.1 and 0.2? +4.14
Understanding z3 bvsmod behavior with SSA +4.06
Get fractional part of real in QF_UFNRA 0.00
Getting the domain of an Int with z3 0.00
Can we restrict a range of values for each variable in z3? 0.00
Simplifying CNF formula while preserving all solutions wrt certain... -1.97
Z3Py: Create model object 0.00
How to declare constraints with variable as array index in Z3Py? +2.00
How to declare constraints with variable as array index in Z3Py? -4.00
How to declare constraints with variable as array index in Z3Py? +2.00
Right-tightening ArrowLoop law 0.00
Z3 ForAll on Arrays 0.00
Records with Z3 0.00
Prove a Boolean formula under some Implies conditions in z3py 0.00
Z3 quantified formula with implication giving unsat 0.00
Z3 Doesn't Recognize Insert and Nil Without Type 0.00
Automatically deriving Provable for predicates over records in SBV -2.43
Sum of all the bits in a Bit Vector of Z3 -3.72
Simplify function interpretation in model 0.00
SMT: check uniqueness and totality of function 0.00
Why Z3 always return unknown when assertions have power? 0.00
Implicit vs explicit existential quantification in SMT formulas 0.00
Bitvector arithmetics on Z3 0.00
is z3 ignoring some of my restrictions? 0.00
Why does this SBV code stop before hitting the limit I set? 0.00
How do I get symbolic square root and logarithm functions in SBV? 0.00
Can we define relations in Z3? -3.59
How to correctly use Solver() command in Python API of Z3 with decl... +4.13
Simplifying an expression leads to time out +4.33
Defining Rules for Bit Vectors in SMT2 0.00
z3py: What is a correct way of asserting a constraint of "some... 0.00
Avoiding non-linearity using bit-vectors in z3 0.00
Symbolic theory proving using SBV and Haskell +4.00
Symbolic theory proving using SBV and Haskell -4.00
Segmentation fault in Z3 (Haskell) -3.90
Z3 int2bv operation +0.04
Incorrect result with Z3 SMT and Python -2.40
Directly generating specific subsets of a powerset? -3.30