@@ -12,7 +12,7 @@ Z3 can be built using Visual Studio Command Prompt and make/g++.
2) Building Z3 using make/g++ and Python
Id #80 | Release:
| Updated: Today at 6:19 PM by idudka | Created: Today at 6:19 PM by idudka
It looks like (pop) doesn't remove functions or sorts from the current scope. The sample problem under "Using Scopes" in this guide has a comment on the final line:
Id #79 | Release:
| Updated: Sat at 1:12 AM by dvitek | Created: Sat at 1:12 AM by dvitek
We sometimes use a logic comprised of QF_ABV plus the "as const" array construct. I recently did an experiment where I extended z3 with a QF_GABV logic (GA = Generalized Arrays). I added...
Id #78 | Release:
| Updated: Nov 26 at 9:10 PM by dvitek | Created: Nov 26 at 9:10 PM by dvitek
In File "src/api/python/z3.py", line 6332, in apply
There is a typo in this line:
p = args2params(arguments, keywords, a.ctx)
a.ctx is used when this should be self.ctx
A patch is attached.
Id #77 | Release:
| Updated: Nov 20 at 5:56 PM by NikolajBjorner | Created: Nov 20 at 2:37 PM by gario
Z3 returns a model with (a==2) for the following constraints, which is an error mathematically speaking. Is this due to non-linear arithmetic limitation?
(declare-const a Int)
(declare-const b Int)...
Id #76 | Release:
| Updated: Nov 13 at 8:00 PM by znajem | Created: Nov 13 at 8:00 PM by znajem
With 89c1785b7322 on mac 10.8 with Xcode 5.0.1 I get the following build error:
clang: warning: argument unused during compilation: '-fopenmp'
clang: warning: argum...
Id #74 | Release:
| Updated: Nov 18 at 5:50 PM by wintersteiger | Created: Oct 28 at 4:46 PM by omarmrivas
In our work with MetiTarski and z3, we use the :timeout option for calls of (check-sat-using). Many repeated calls to z3 (4.3.1) are taking place. With OSX 10.8.5 and XCode 5, if you repeatedly cal...
Id #70 | Release:
| Updated: Oct 15 at 3:25 PM by ic3guy | Created: Oct 15 at 11:21 AM by ic3guy
Hello. Consider the following simple example in Z3Py:
i = IntSort()
b = BoolSort()
p = Function('p', i, b)
g = Function('g', i, i, b)
f = Fixedpoint()
Id #67 | Release:
| Updated: Sep 20 at 6:28 PM by ilyagri | Created: Sep 20 at 6:26 PM by ilyagri
I am working with Z3 and have noticed a strage behaviour while I was working with arrays. Because nobody on Stackoverflow could or wanted to answer my question and the behaviour seems so st...
Id #59 | Release:
| Updated: Aug 1 at 9:28 AM by cliguda | Created: Aug 1 at 9:28 AM by cliguda
I posted a stackoverflow question on this topic; as yet it's unanswered, but my subsequent experience makes me think more and more that this is a bug. Here is the original question:
Id #55 | Release:
| Updated: Jul 16 at 9:12 PM by NikolajBjorner | Created: Jul 15 at 1:09 PM by EfForEffort