StackRating

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

Malte Schwerhoff

Rating
1477.40 (4,505,326th) 		Reputation
9,324 (16,525th)
Page: 1 2 3 ... 5
Title Δ
Describing a function partially in Z3 or Z3py -1.71
Z3: Are functions realized with inlining? 0.00
Solving SAT problem using Z3 without repeating Boolean expression -1.73
Rounded floating-point number comparison issue -1.99
Does multiplying a wildcard in viper mean anything? 0.00
Does lean enhance proof surveyability? 0.00
Invariant fails but assert before loop verifies 0.00
how to use z3 to get valid range of a variable -1.80
Incremental input and assertion sets in Z3 -1.82
Z3 variable name causing "unknown" satisfiability +0.18
How to define a piecewise function in z3 0.00
In PHP does specifying an argument type in a subclass method where... 0.00
Is there a kind of "reference manual" for Z3 -1.84
double permission inhale leads to unexpected verifications 0.00
Scala unused expression error with if statement -1.79
Performance Visibility for Z3 +0.15
Z3 tactic for conjunction elimination in formulas with quantifiers 0.00
Expected error or incompleteness with quantified permissions and wi... 0.00
Which SMT-LIB attributes does Z3 support, and why? 0.00
defining list concat in smtlib +0.16
forall usage in SMT -1.86
Z3Py solver producing different results in Jupyter 0.00
Extracting upper and/or lower bound of a numerical variable in Z3 -0.03
Pip install from git repository, errors due to wrong quotes 0.00
What's an inductive invariant for this piece of code? -1.89
Why does introducing this existential quantifier cause non-terminat... 0.00
How to understand what z3 is doing when it loops? 0.00
Writing a computer program that will analyse the quality of another... +2.37
Quantifier-free way to specify constructor of Z3 sum type 0.00
Encoding partial maps in Z3 0.00
Z3 might be inconsistent when solving this string problem? 0.00
Guarantees about partial model when check-sat returns unknown 0.00
Map data structure in Z3 -1.99
Cyclic relation in Datalog using SMTLib for z3 0.00
Z3 query with existential quantifier return wrong result 0.00
Performance issues with z3py using modulo and optimization -0.01
Dafny, call may violate context's modifies clause -0.47
Guiding z3's proof search 0.00
Defining algebraic datatypes with constraints in Z3 -0.02
Arithmetic conflicts vs conflicts in Z3 solver statistics 0.00
Creating List in z3 using function 0.00
Equilvalent of array store for a record 0.00
How do you extract an element as the base type from a Seq type in Z3? +1.99
z3py: Usage of existential quantifier 0.00
How would you implement dereferencing of pointers in z3 0.00
Correct syntax for newline in Github Bio -0.49
Why is this simple Z3 proof so slow? 0.00
Unsafe scripts using pelican 0.00
Boogie strange assert(false) behavior 0.00
Boogie on Visual Studio -0.48