StackRating

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

Nikolaj Bjorner

Rating
1520.42 (31,060th) 		Reputation
7,321 (21,820th)
Page: 1 2 3 4 5 6 7
Title Δ
Z3 maximization API: possible bug? 0.00
Models and recursive functions 0.00
Z3 - How to extract variables from a given formula? 0.00
Quantifier elimination in the real closed fields in Z3 (Python) 0.00
How to define enumerated types in SMT-LIB for Z3 0.00
Random seed for Z3 SAT Solver 0.00
How to extract sub-formulas(predicates, terms) in Z3 efficiently? 0.00
How to get all the variables that were added to any constraint in a... 0.00
Z3 C++ API expression predicate operator overload does not have uns... 0.00
Z3 is the only system that is able to prove REL052+1.p? 0.00
What is the "official" version of the PDR engine in Z3? 0.00
Z3 Command-line Timeout 0.00
precompiled version that supports HORN? 0.00
What commandline is used for Z3 in rise4fun? 0.00
Z3 Maximise and Conflicts 0.00
Dose SMTLIB 1.2 has a (get-value) function like like SMTLIB 2 0.00
Use of "for all" with Uninterpreted sorts JAVA API +0.48
Exclusive datatypes in z3 (follow up) 0.00
Z3 opt-context in the opt-branch 0.00
Which is better practice in SMT: to add multiple assertions or sing... 0.00
Mixing Z3 c and c++ apis 0.00
Z3 Maximize in C++ +0.48
Z3 C-API Get value of a const with no constraints 0.00
Encoding "at-most-k / at-least-k booleans are true" const... 0.00
Use of random-seeds in Z3 0.00
Performance issues about Z3 for Java 0.00
Z3: How to best encode a "switch statement"? -0.02
Simplex in z3 via for-all 0.00
z3 with workflow satisfiability 0.00
Function receiving sort with 2 parameters in the constructor 0.00
fun in Z3 returning more than one element 0.00
Most efficient way to represent memory buffers in Z3 0.00
How to get multiple constraints in Z3 Fixedpoint? 0.00
muZ3: Non-deterministic recursive call 0.00
DPLL(T) algorithm used in Z3 (linear arithmetic) 0.00
Which logics are supported by z3? 0.00
Z3: Parse Term from String 0.00
incremental solving with nlsat solver 0.00
How to find Lagrange Interpolation Polynomial with Z3 in Python? 0.00
Is there any way to get the coefficient values from an SMT expressi... 0.00
(set-option :macro-finder true): does not work in a theorem of grou... -0.03
possible to extract an unsat core when using 'nlsat' solver 0.00
Does Z3 have a feature for facilitating the matching of subformulas... 0.00
Possible bug with Z3: Z3 is not able to prove a theorem in Topology 0.00
Sum array in z3 solver 0.00
mysterious 'unknown' from Z3 0.00
Is it possible to cast a bitvector of one bit into a boolean variab... -0.32
extracting value from a model in exists_expr_vector_example 0.00
How to calculate Absolute value in z3 or z3py +4.09
use of define-fun in z3's input language 0.00