active questions tagged z3 - Stack Overflow News Feed 
Thursday, January 29, 2015  |  From active questions tagged z3 - Stack Overflow




Consider the following SMTLIB program (on rise4fun here):



(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)

(declare-const n Int)
(declare-const i Int)
(declare-const r Int)

(assert (= i n))
(assert (= r (* i n)))

(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)


Although it appears to only require reasoning with syntactic equality, Z3 (4.3.2 official release, and also 4.4.0 b6c40c6c0eaf) nevertheless fails to show that the final assertion is unsat.



Unexpectedly (at least for me), setting smt.arith.nl.gb to true makes the example verify (i.e. the check-sat yields unsat).



For what it's worth, here are some further observations:



  • The final assertion can be shown unsat if the multiplication is changed to (* i n) or (* n i), respectively

  • It cannot be shown unsat if the multiplication is changed to (* i i)

  • (push) and (pop) don't appear to affect the example, i.e. they can be removed without affecting the described observations


Is this a bug or is there a reason that smt.arith.nl.gb is required to show this example unsat?



Thursday, January 29, 2015  |  From active questions tagged z3 - Stack Overflow




I'm using Scala^Z3 for using Z3 within Scala. Now for some experiments I'm doing, which involves solving problems which become very complex, in order to cancel the current calculation.



I have tried a soft timeout, which from the documentation sounded like the perfect option for me. I used it like this:



config.setParamValue("SOFT_TIMEOUT", "5200")


However, instead of just canceling the calculation, it crashes my whole Scala program with the error message "Error: invalid usage".



I've tried to use concurrency like Futures in order to prevent the main program to die, but then I can't use Z3 in my program anymore until I restart it, because I get the error message "Error: invalid usage" immediately.



Is there something I misunderstood about soft timeouts?



Thanks in advance!



Yours,
Stefan Tiran



Wednesday, January 28, 2015  |  From active questions tagged z3 - Stack Overflow




Consider the following SMTLIB program (on rise4fun here):



(set-option :auto_config false)
(set-option :smt.mbqi false)
(set-option :smt.arith.nl.gb false)

(declare-const n Int)
(declare-const i Int)
(declare-const r Int)

(assert (= i n))
(assert (= r (* i n)))

(push)
(assert (not (= r (* n n))))
(check-sat) ; unknown
(pop)


Although it appears to only require reasoning with syntactic equality, Z3 (4.3.2 official release, and also 4.4.0 b6c40c6c0eaf) nevertheless fails to show that the final assertion is unsat.



Unexpectedly (at least for me), setting smt.arith.nl.gb to true makes the example verify (i.e. the check-sat yields unsat).



For what it's worth, here are some further observations:



  • The final assertion can be shown unsat if the multiplication is changed to (* i n) or (* n i), respectively

  • It cannot be shown unsat if the multiplication is changed to (* i i)

  • (push) and (pop) don't appear to affect the example, i.e. they can be removed without affecting the described observations


Is this a bug or is there a reason that smt.arith.nl.gb is required to show this example unsat?



Tuesday, January 27, 2015  |  From active questions tagged z3 - Stack Overflow




This is the reduction of a more interesting problem, in which the missing property was (for positive k,M and N), that ((k % M) * N) < M*N. Below is an encoding of the simpler problem that a <= b ==> (a*c) <= (b*c). Such a query succeeds (we get unsat), but if the expression b is replaced by b+1 (as in the second query below) then we get unknown, which seems surprising. Is this the expected behaviour? Are there options to improve the handling of such inequalities? I tried with and without configuration options, and various versions of Z3, including the current unstable branch. Any tips would be much appreciated!



(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (> a 0))
(assert (> b 0))
(assert (> c 0))
(assert (<= a b))
(assert (not (<= (* a c) (* b c))))
(check-sat)
(assert (<= a (+ b 1)))
(assert (not (<= (* a c) (* (+ b 1) c))))
(check-sat)


Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




is the information on this page still up to date?



http://leodemoura.github.io/blog/2012/12/10/z3-for-java.html



I see that both rc and stable have a examples/java folder with an actual example,



does it mean that java bindings are now part of the stable/rc branch?



How can I enable and build them?



Regards,



Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




Is there any relation between the configuration option smt.arith.nl.rounds and the statistics value final-checks (or is it just a coincidence that the description of the former mentions "final checks")?



I ran Windows x64 builds of Z3 4.3.2 (official download) and of Z3 4.4 0ab54b9e0c33 on an SMTLIB program, and in both cases the reported number of final-checks (around 10,000) appears to be unaffected by whichever value I choose for smt.arith.nl.rounds (I tried 1, 64, 128, ..., 1024 and 4096).



Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




Giving for example:
context ctx;



sort type1 = ctx.int_sort();
sort type2 = ctx.bool_sort();

func_decl b1 = function("b1", type1, type2);

expr x = c.int_const("x");
expr y = c.int_const("y");
expr z = c.int_const("z");

ctx.add(b1(x));
ctx.add(b1(y));
ctx.add(b1(z));


How can one declare x, y and z as distinct other than using:
s.add(not(x==y or x==z or y==z));
?



Thank you.



Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




For my application code, I used the following settings for z3 params for my solver



   z3::params p(context);
   p.set(":relevancy", static_cast<unsigned>(1));
   p.set(":logic", QF_ABV);
   p.set(":timeout", timeout); 
   solver.set(p);


After updating to latest Z# unstable I got C++ exceptions essentially stating that logic and timeout are not valid parameters. I did not find any equivalent option for logic, so I assume that is being deduced automatically. However, for timeout, there are two options soft_timout and solver2_timeout. I know that solver2_timeout is used for incremental solver (ie. with push/pops), hence I changed the code to use the following parameters.



 z3::params p(context);
 p.set(":relevancy", static_cast<unsigned>(1));
 p.set(":soft_timeout", yices_timeout); 
 solver.set(p)


Is the change correct? How is soft_timeout different from timeout? Is there a documentation for valid "z3::params" maintained somewhere?



Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




Giving for example:
context ctx;



sort type1 = ctx.int_sort();
sort type2 = ctx.bool_sort();

func_decl b1 = function("b1", type1, type2);

expr x = c.int_const("x");
expr y = c.int_const("y");
expr z = c.int_const("z");

ctx.add(b1(x));
ctx.add(b1(y));
ctx.add(b1(z));


How can one declare x, y and z as distinct other than using:
s.add(not(x==y or x==z or y==z));
?



Thank you.



Monday, January 26, 2015  |  From active questions tagged z3 - Stack Overflow




For my application code, I used the following settings for z3 params for my solver



   z3::params p(context);
   p.set(":relevancy", static_cast<unsigned>(1));
   p.set(":logic", QF_ABV);
   p.set(":timeout", timeout); 
   solver.set(p);


After updating to latest Z# unstable I got C++ exceptions essentially stating that logic and timeout are not valid parameters. I did not find any equivalent option for logic, so I assume that is being deduced automatically. However, for timeout, there are two options soft_timout and solver2_timeout. I know that solver2_timeout is used for incremental solver (ie. with push/pops), hence I changed the code to use the following parameters.



 z3::params p(context);
 p.set(":relevancy", static_cast<unsigned>(1));
 p.set(":soft_timeout", yices_timeout); 
 solver.set(p)


Is the change correct? How is soft_timeout different from timeout? Is there a documentation for valid "z3::params" maintained somewhere?



Sunday, January 25, 2015  |  From active questions tagged z3 - Stack Overflow




Two questions:



1)
I want to know what sort of SMT-LIB2 instances will cause Z3 to take a long time. I know bit vector multiplication can be pretty slow and transcendental equations { x = sin(x) } cannot be solved. Is there any classification of problems whose performance hits most orders of magnitude?



2)
Z3 can handle non-linear arithmetic like { x^3 = 2 } but I want to know the limitations and for what problems will it struggle to produce an answer/model?



Thank you.



Sunday, January 25, 2015  |  From active questions tagged z3 - Stack Overflow




Given the following simplified quantifiers, with the Z3 options set according to those generated by Boogie (full details below), I get "unknown" as a result:



(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
  :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
  (G x) (F x))
  :pattern ((F x))
))))
(check-sat)


My understanding for what (I think) Z3 would do with this problem, is skolemise the existential (not forall), which would yield ground instances of both F and G. Given these in the e-graph, we should be able to instantiate the other quantifier, and get unsat. I can see that Z3 probably has to case-split to do this, but I would expect this case-splitting to take place after removing the quantifier and populating the e-graph.



Instead, the first quantifier doesn't get instantiated in the above problem. I've made a number of observations:



  1. Swapping the order of the (F x) and (G x) terms in the first quantifier results in "unsat" without any quantifier instantiations (I suppose some simplification spots the similarity between the two quantified assertions?).
  2. Swapping the order of the (G x) and (F x) terms in the second quantifier (as well as those in the first) results in "unsat" with a single quantifier instantiation (which is the behaviour I'd expect in general).
  3. Changing the smt.case_split option affects the behaviour. Set to 3 (as chosen by Boogie) or 5, we get "unknown". Set to 0,1,2 or 4, I get "unsat".

It would be great to understand the scenarios above, and why (in the failing cases) these terms don't always make it to the e-graph after skolemisation. I'm not sure what the effects of changing the case_split option are in general. At the moment, I don't think Boogie allows that to be changed (and overrides any choice made on the command-line). But I have the feeling that the e-graph should get the information in all cases, ideally.



Here's the full file (removing most of the options set doesn't seem to make a difference to the failing cases, except for the smt.case_split one):



(set-option :print-success false)
(set-info :smt-lib-version 2.0)
(set-option :AUTO_CONFIG false)
;(set-option :MODEL.V2 true)
(set-option :smt.PHASE_SELECTION 0)
(set-option :smt.RESTART_STRATEGY 0)
(set-option :smt.RESTART_FACTOR |1.5|)
(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)
(set-option :smt.DELAY_UNITS true)
(set-option :NNF.SK_HACK true)
(set-option :smt.MBQI false)
(set-option :smt.QI.EAGER_THRESHOLD 100)
(set-option :smt.QI.COST |"(+ weight generation)"|)
(set-option :TYPE_CHECK true)
(set-option :smt.BV.REFLECT true)
(set-option :TIMEOUT 0)
(set-option :smt.QI.PROFILE true)
(set-option :smt.CASE_SPLIT 3)
; done setting options


(declare-fun F (Int) Bool)
(declare-fun G (Int) Bool)

(assert (forall ((x Int)) (! (and
  (F x) (G x))
   :pattern ((F x))
)))
(assert (not (forall ((x Int)) (! (and
(G x) (F x))
  :pattern ((F x))
))))
(check-sat)


Friday, January 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am trying to build 32-bit z3 on a 64-bit linux system. I need to do this to get a 32-bit libz3.so, that I can use with my 32-bit application. I changed the phython file scripts/mk_util.py to add -m32 flag to various compiler and linker flags. I am able to build z3 using these steps from the z3 folder:
python scripts/mk_make.py; cd build; make



Then, I call make examples to build c and cpp_examples. However, when I run cpp_example, I get segmentation fault. Following is the backtrace for the segmentation fault:



#0  0x00c95463 in goal::quick_process(bool, expr*&, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#1  0x00c97b04 in goal::update(unsigned int, expr*, app*, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#2  0x00c0e3c8 in simplify_tactic::imp::operator()(goal&) () from ./libz3.so
#3  0x00c0d55f in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#4  0x00c88eeb in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#5  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#6  0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#7  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#8  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#9  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#10 0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#11 0x00c8f40d in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#12 0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#13 0x00c81b8a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from ./libz3.so
#14 0x00c8240a in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::basic_string<char, std::char_traits<char>, std::allocator<char> >&) () from ./libz3.so
#15 0x00b3b5af in tactic2solver::check_sat_core(unsigned int, expr* const*) () from ./libz3.so
#16 0x00b3cddc in solver_na2as::check_sat(unsigned int, expr* const*) () from ./libz3.so
#17 0x00b3a40d in combined_solver::check_sat(unsigned int, expr* const*) () from ./libz3.so
#18 0x00448808 in _solver_check () from ./libz3.so
#19 0x00448e2f in Z3_solver_check () from ./libz3.so
#20 0x0805a32a in z3::solver::check() ()
#21 0x0804b542 in find_model_example1() ()
#22 0x08056638 in main ()


I am using Linux version 2.6.32-504.1.3.el6.x86_64, g++ 4.4.7, python 2.7 and z3's latest unstable commit 48c72d2 (2015-01-23 | FPA API: naming consistency (HEAD, origin/unstable, unstable) [Christoph M. Wintersteiger]). Here is the diff to the scripts/mk_util.py file.



diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4641a7b..e6decc0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -27,10 +27,10 @@ def getenv(name, default):

 CXX=getenv("CXX", None)
 CC=getenv("CC", None)
-CPPFLAGS=getenv("CPPFLAGS", "")
-CXXFLAGS=getenv("CXXFLAGS", "")
+CPPFLAGS=getenv("CPPFLAGS", "-m32")
+CXXFLAGS=getenv("CXXFLAGS", "-m32")
 EXAMP_DEBUG_FLAG=''
-LDFLAGS=getenv("LDFLAGS", "")
+LDFLAGS=getenv("LDFLAGS", "-m32")
 JNI_HOME=getenv("JNI_HOME", None)

 CXX_COMPILERS=['g++', 'clang++']
@@ -1523,7 +1523,7 @@ def mk_config():
         check_ar()
         CXX = find_cxx_compiler()
         CC  = find_c_compiler()
-        SLIBEXTRAFLAGS = ''
+        SLIBEXTRAFLAGS = '-m32'
         if GPROF:
             CXXFLAGS = '%s -pg' % CXXFLAGS
             LDFLAGS  = '%s -pg' % LDFLAGS
@@ -1572,7 +1572,7 @@ def mk_config():
             OS_DEFINES     = '-D_LINUX'
             SO_EXT         = '.so'
             LDFLAGS        = '%s -lrt' % LDFLAGS
-            SLIBFLAGS      = '-shared'
+            SLIBFLAGS      = '-shared -m32'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'FreeBSD':
             CXXFLAGS       = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS


Friday, January 23, 2015  |  From active questions tagged z3 - Stack Overflow




I am trying to build 32-bit z3 on a 64-bit linux system. I need to do this to get a 32-bit libz3.so, that I can use with my 32-bit application. I changed the phython file scripts/mk_util.py to add -m32 flag to various compiler and linker flags. I am able to build z3 using these steps from the z3 folder:
python scripts/mk_make.py; cd build; make



Then, I call make examples to build c and cpp_examples. However, when I run cpp_example, I get segmentation fault. Following is the backtrace for the segmentation fault:



#0  0x00c95463 in goal::quick_process(bool, expr*&, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#1  0x00c97b04 in goal::update(unsigned int, expr*, app*, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#2  0x00c0e3c8 in simplify_tactic::imp::operator()(goal&) () from ./libz3.so
#3  0x00c0d55f in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#4  0x00c88eeb in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#5  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#6  0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#7  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#8  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#9  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#10 0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#11 0x00c8f40d in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#12 0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#13 0x00c81b8a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from ./libz3.so
#14 0x00c8240a in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::basic_string<char, std::char_traits<char>, std::allocator<char> >&) () from ./libz3.so
#15 0x00b3b5af in tactic2solver::check_sat_core(unsigned int, expr* const*) () from ./libz3.so
#16 0x00b3cddc in solver_na2as::check_sat(unsigned int, expr* const*) () from ./libz3.so
#17 0x00b3a40d in combined_solver::check_sat(unsigned int, expr* const*) () from ./libz3.so
#18 0x00448808 in _solver_check () from ./libz3.so
#19 0x00448e2f in Z3_solver_check () from ./libz3.so
#20 0x0805a32a in z3::solver::check() ()
#21 0x0804b542 in find_model_example1() ()
#22 0x08056638 in main ()


I am using Linux version 2.6.32-504.1.3.el6.x86_64, g++ 4.4.7, python 2.7 and z3's latest unstable commit 48c72d2 (2015-01-23 | FPA API: naming consistency (HEAD, origin/unstable, unstable) [Christoph M. Wintersteiger]). Here is the diff to the scripts/mk_util.py file.



diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4641a7b..e6decc0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -27,10 +27,10 @@ def getenv(name, default):

 CXX=getenv("CXX", None)
 CC=getenv("CC", None)
-CPPFLAGS=getenv("CPPFLAGS", "")
-CXXFLAGS=getenv("CXXFLAGS", "")
+CPPFLAGS=getenv("CPPFLAGS", "-m32")
+CXXFLAGS=getenv("CXXFLAGS", "-m32")
 EXAMP_DEBUG_FLAG=''
-LDFLAGS=getenv("LDFLAGS", "")
+LDFLAGS=getenv("LDFLAGS", "-m32")
 JNI_HOME=getenv("JNI_HOME", None)

 CXX_COMPILERS=['g++', 'clang++']
@@ -1523,7 +1523,7 @@ def mk_config():
         check_ar()
         CXX = find_cxx_compiler()
         CC  = find_c_compiler()
-        SLIBEXTRAFLAGS = ''
+        SLIBEXTRAFLAGS = '-m32'
         if GPROF:
             CXXFLAGS = '%s -pg' % CXXFLAGS
             LDFLAGS  = '%s -pg' % LDFLAGS
@@ -1572,7 +1572,7 @@ def mk_config():
             OS_DEFINES     = '-D_LINUX'
             SO_EXT         = '.so'
             LDFLAGS        = '%s -lrt' % LDFLAGS
-            SLIBFLAGS      = '-shared'
+            SLIBFLAGS      = '-shared -m32'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'FreeBSD':
             CXXFLAGS       = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS


Wednesday, January 21, 2015  |  From active questions tagged z3 - Stack Overflow




Is there any relation between the configuration option smt.arith.nl.rounds and the statistics value final-checks (or is it just a coincidence that the description of the former mentions "final checks")?



I ran Windows x64 builds of Z3 4.3.2 (official download) and of Z3 4.4 0ab54b9e0c33 on an SMTLIB program, and in both cases the reported number of final-checks (around 10,000) appears to be unaffected by whichever value I choose for smt.arith.nl.rounds (I tried 1, 64, 128, ..., 1024 and 4096).



Wednesday, January 21, 2015  |  From active questions tagged z3 - Stack Overflow




Running Windows x64 builds of Z3 4.3.2 (official download) and Z3 4.4 0ab54b9e0c33 on this program (which is unfortunately quite long) yields an invalid rational value passed as an integer.



The problem does not appear to be a type checker problem, because the apparently offending formula (the last check-sat in the program) looks fine type-wise:



(declare-const i@99 Int)
(declare-const k@38 Int)
...
(assert (not (and (<= 0 i@99) (< i@99 (+ k@38 1)))))
(check-sat) ; ERROR


My guess is that the problem occurs during proof search because marginally changing the program makes the error disappear. I experimented with changing Z3's configuration options and observed that the error disappears if smt.arith.nl is set to false, respectively, if smt.qi.eager_threshold is set to a value lower than 10. Moreover, removing essentially any push-pop scope preceding the last check-sat also makes the error disappear (I didn't actually try to remove every single scope, though). Both observations make me believe that the error is raised during proof search and in an "area" of the search space that is only reached under specific circumstances.



The offending line as well as lines I experimented with are marked by [XXX].



Is this a bug or is something else going on here?



Tuesday, January 20, 2015  |  From active questions tagged z3 - Stack Overflow




I might have found a configuration bug related to mbqi. Consider the following, short program:



(set-option :smt.mbqi true)
  ; Set to false and the warnings disappear
(set-option :smt.relevancy 2)
  ; On my local machine I got
  ;   0 and 1 - three times the same warning
  ;   2 (or higher) - one warning
  ; but on rise4fun I always got the same warning three times
(set-option :smt.case_split 3)
  ; WARNING: relevacy must be enabled to use option CASE_SPLIT=3, 4 or 5

(declare-fun fun (Int) Bool)
(assert (forall ((x Int)) (fun x)))

(check-sat)


Running it locally using the official download build of Z3 4.3.2 on Windows 7 x64 I get unexpected warnings about relevancy not being enabled. Changing the value for relevancy only affects how many warnings I get (three or one).



Running the script on rise4fun always yields three times the same warning, regardless of the value chosen for relevancy.



Is this actually a bug or am I missing something here?



Tuesday, January 20, 2015  |  From active questions tagged z3 - Stack Overflow




Q1: Is it possible to query the times Z3 spent in different sub-solvers?



Calling (get-info :all-statistics) gives the overall run time of Z3, but I would like to break it down into individual sub-solvers.



I am particularly interested in the time spent in arithmetic-related sub-solver, more precisely, in those that give rise to the statistics grobner and nonlinear-horner.





Q2: Furthermore, is it possible to put a timeout on sub-solver?



I could imagine something like defining a timeout per check-sat and sub-solver that bounds the time Z3 can spent in that sub-solver. Z3 would repeatedly call n different sub-solvers, and if the time bound of one of them is reached it continues, but only uses the remaining n-1 sub-solvers.



I read the tactics tutorial and got the impression that this might actually be possible by something along the lines of



(repeat
  (par-or
    (try-for <arithmetic-solvers> 500)
    <all-other-solvers>))


but I couldn't figure out which solvers to use.



Tuesday, January 20, 2015  |  From active questions tagged z3 - Stack Overflow




General problem



I've noticed several times that push-pop scopes that have already been popped appear to affect the time that a check-sat in a subsequent scope needs.



That is, assume a program with multiple (potentially arbitrarily nested) push-pop scopes, each of which contain a check-sat command. Furthermore, assume that the second check-sat takes 10s, whereas the first one takes only 0.1s.



...
(push)
  (assert (not P))
  (check-sat) ; Could be sat, unsat or unknown
(pop)
...
(push)
  (assert (not Q))
  (check-sat) ; Could be sat, unsat or unknown
(pop)


After commenting the first push-pop scope, the second check-sat only takes 1s. Why is that?



  • AFAIK, Z3 switches to incremental solvers if push-pop scopes are used. Is there a (conceptual) reason for why they might behave this way?

  • I was told once that Z3 attributes symbols by importance, which affects proof search (and the importance of a symbol can also change during proof search). Could that be the reason? Is it possible to reset importance (in between scopes)?

  • Could it be a bug? I found this post where Leonardo mentions a bug that seems related (his answer is from 2012, though).

Particular instance



I unfortunately only have fairly long (automatically generated) SMTLib files that illustrate the behaviour, one of which you can find as this gist. It uses quantifiers and uninterpreted functions, but neither mbqi nor arrays or bit vectors. The example consists of 148 nested push-pop scopes and 89 check-sats, and it takes Z3 4.3.2 about 8s to process it. The last check-sat (prefixed by an echo) takes by far the longest.



I randomly commented several push-pop scopes (one at a time, never the last one, make sure you don't comment symbol declarations), and in most cases, the overall run time went down to less than 1s. That is, the last check-sat was done significantly faster.



To provide further details, I compared a run of Z3 with all scopes (slow, 8s) with a run of Z3 where the scope marked by [XXX] had been commented (fast, 0.3s). The results can be seen in this diff (left is slow, right is fast).



The diff shows that all check-sats behave the same (I faked the commented one by echo'ing "unsat"), from which I conclude that the commented scope affects the proof search, but not its final outcome.



I also tried to make some sense out of differences in the obtained statistics, but I know very little about how to interpret the statistics correctly. Here are the few statistics I could make sense of:



  • grobner (383 vs 36) and nonlinear-horner (342 vs 25), so it seems that the slower run performs more arithmetic-related operations. The commented scope is indeed about to non-linear arithmetic (and so are lots of others), but the particular proof in the commented scope should be "trivial", it is essentially showing that x != 0 for an x about which 0 < x has been assumed explicitly.

  • memory (40 vs 7), which I interpret as indicating that Z3 explores a larger search space in the slow version of the program

  • quant-instantiations (43k vs 51k), which surprised me because the significantly faster run nevertheless triggered notably more quantifier instantiations.


Tuesday, January 20, 2015  |  From active questions tagged z3 - Stack Overflow




Q1: Is it possible to query the times Z3 spent in different sub-solvers?



Calling (get-info :all-statistics) gives the overall run time of Z3, but I would like to break it down into individual sub-solvers.



I am particularly interested in the time spent in arithmetic-related sub-solver, more precisely, in those that give rise to the statistics grobner and nonlinear-horner.





Q2: Furthermore, is it possible to put a timeout on sub-solver?



I could imagine something like defining a timeout per check-sat and sub-solver that bounds the time Z3 can spent in that sub-solver. Z3 would repeatedly call n different sub-solvers, and if the time bound of one of them is reached it continues, but only uses the remaining n-1 sub-solvers.



I read the tactics tutorial and got the impression that this might actually be possible by something along the lines of



(repeat
  (par-or
    (try-for <arithmetic-solvers> 500)
    <all-other-solvers>))


but I couldn't figure out which solvers to use.



 active questions tagged z3 - Stack Overflow News Feed 

Last edited Nov 23, 2012 at 5:52 AM by leodemoura, version 13

Comments

No comments yet.