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 ... 7

Title	Δ
Z3 - How to set a byte constraint on a BitVec	-0.08
z3py: simplify nested Stores with concrete values	0.00
z3 and νz (z3opt): setting logic using the Python API	0.00
Z3Py: add constraint of two vectors inequality	0.00
Advantages of using OpenMP in Z3 nix version	0.00
Why does the z3 smt prover fail for such a simple formula?	0.00
Z3Py: constraint of not equal tuples	0.00
How to print out the whole symbolic expression in Z3?	0.00
Using z3 api to solve LRA runs slower than use z3 in terminal	0.00
Defining a Theory of Sets with Z3 using C++	0.00
z3: set-logic unexpected behavior for scientific notation	0.00
Does using quantifier affect the performance of Z3?	0.00
unknown when using a integer division in z3 smt2	0.00
Simulate the semantics of x86 opcode 'bsf' in Z3	0.00
Efficient method to store z3 symbolic expression into the key of a...	0.00
Z3-solver throws 'model is not available' exception on pyth...	0.00
∃-queries and ∀-queries with Z3 fixedpoint engine	0.00
Z3: Translate a BoolRef into a BitVecVal	0.00
Z3 giving unexpected UNSAT for forall formulas	0.00
Sum of all the bits in a Bit Vector of Z3	+0.46
Z3 Output of get-value	0.00
Executing get-model or unsat-core depending on solver's decision	+0.50
Implement arithmetic equal in Z3	0.00
Microsoft Z3 Dot Net API, Cloning Solver	0.00
Unsat core from Z3 (version 4)	0.00
What is the c++ file and method where the DPLL algorithm backtraces...	0.00
Z3 optimization: detect unboundedness via API	0.00
Changing order of Z3 fixepoint queries changes the result	0.00
Using define-fun-rec in SMT	-0.02
Assign value to bool variable in Z3 C api	0.00
Z3Opt C++ API: parse smtlib2 formula from file	0.00
Running time analysis of Z3	0.00
Z3 Optimizer Unsatisfiability with Real Constraints Using C++ API	-0.52
Can Z3 effectively solve constraints with a max operation?	+0.48
Can Z3 call an externally defined function?	0.00
Seg fault while creating an array of Z3_ast from Z3_ast_vector	0.00
Z3 Python multiply two bitvectors	0.00
Failed qfnra-nlsat prevents other tactics?	0.00
Undocumented trigonometric functions in Z3 reparable?	0.00
Satisfiability of a formula having forall quantifier	0.00
Why can't Z3 prove/admit that `is_int` is closed under some ope...	0.00
Do Max-SMT benefit from incremental solving?	0.00
Equivalent of "store" operator for Records in z3	0.00
Z3 should be able to verify this program?	+0.48
Using MaxSAT Queries in Z3	0.00
Implementing arrays in Z3 timeout	0.00
Duplicate a Z3Context	0.00
Bounding universally quantified variable	0.00
Why result of Z3 online and Z3PY are different?	-2.09
how to parse smt2 commands using z3 api c++?	0.00