StackRating

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

Christoph Wintersteiger

Rating
1497.94 (3,911,093rd) 		Reputation
6,994 (22,962nd)
Page: 1 2 3 4 5 6 ... 7
Title Δ
Error adding containts to solver in z3 0.00
Z3 segmentation fault and non-numerical results 0.00
Segmentation fault on a model using only EUF 0.00
Java API push and pop for smt2 file 0.00
how to solve equation instead of giving one model in z3 0.00
Z3 Managed Exception : Java API while trying to use propagate-ineqs... +0.50
Z3 return different answers WITH and WITHOUT using push/pop? 0.00
ASSERTION VIOLATION i==0 ||!is_numeral(args[i]) in Z3 c++ API 0.00
Solving formulas in parallel with z3 0.00
Are existential quantifiers nested under foralls skolemised once? W... 0.00
z3 SMT solver performance on different platforms 0.00
How do I find the memory consumed in modeling/checking the satisfia... +0.08
Z3 bitvector operations +0.49
Z3 Java API - ignoring an expression like a max-function 0.00
Z3 Java API defining a function +0.50
QF_AUFBV instance has one incredibly difficult assumption 0.00
Error while using Z3 module in OCaml 0.00
Compile z3 on Raspberry 0.00
How to define piece-wise functions in Z3py 0.00
z3py error when converting int to bitvec 0.00
Are Z3's previous releases also on MIT license? 0.00
constants in z3 – segmentation fault in c++ api 0.00
How to make up a new bitvec out of existing bitvecs? 0.00
Where can I get windows/linux binaries for Z3opt +0.50
Solvability of nonlinear real arithmetic with premises 0.00
Tracking nonlinear real arithmetic assertions using implications ve... 0.00
Different check-sat answers when asserting same property in between +0.09
Are soft constraints disjunctions? 0.00
Asserting constraint on matrix multiplication 0.00
Getting Unsat Core in Z3 using C++, with Z3_parse_smtlib2_string 0.00
Simplifying expression involving variables in finite domain 0.00
Are statistics accumulated across multiple check-sats? 0.00
Segmentation fault while using par-or tactic 0.00
Checkpoint mechanism for Z3 0.00
(check-sat) vs (check-sat-using smt) 0.00
Modeling constraints in Z3 and Unsat core cases 0.00
function to get nibbles using Z3 and bitvector theory 0.00
Z3: eliminate don't care variables 0.00
Z3:unknown result in Z3 C API 0.00
Unexpected effect of smt.arith.nl.gb on reasoning with (syntactic)... 0.00
How to declare constants as distinct using the z3 c++ API 0.00
Are C++ parameters :logic and :timeout deprecated in Z3 unstable br... 0.00
Running 32-bit z3 on 64-bit linux systems 0.00
Relation between arith.nl.rounds and final-checks 0.00
Measure and bound time spent in arithmetic sub-solvers 0.00
Potential configuration bug in Z3 4.3.2 0.00
Why do already popped scopes affect the check-sat time in subsequen... 0.00
Z3 performance: many assertions vs large conjunction 0.00
Z3 : Questions About Z3 int2bv? 0.00
Distinct in z3 SMT and python 0.00