Inconsistent (check-sat) result between Java API and commandline-tool

[facferreira]

Hi, using the Java API I'm adding assertions, to which I check if they are satisfiable, expecting the Java API to return unsat. However, the Java API is returning unknown (due to incomplete quantifiers) but when I save in a file the result of solver.toString() (that produced the unknown result) and adding a (check-sat) to the file, in the commandline-tool it returns unsat as I expected.

Here is the result of solver.toString():

(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (type String) (id Int) (representations Value) (identifiers Value)))))
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (type String) (id Int) (representations Value) (identifiers Value)))))
(declare-datatypes () ((ValueOption (NoValue) (SomeValue (of_SomeValue Value)))))
(declare-sort IVMap)
(declare-sort SVMap)
(declare-datatypes () ((General (G_Boolean (of_G_Boolean Bool)) (G_Integer (of_G_Integer Int)) (G_String (of_G_String String)) (G_Null))))
(declare-sort SVMap)
(declare-sort IVMap)
(declare-datatypes () ((Value (G (out_G General)) (E (out_E SVMap)) (C (out_C IVMap)) (R (type String) (representations Value) (identifiers Value)))))
(declare-fun r_resourceidof (Value Value) Value)
(declare-fun v_contains (Value Value) Value)
(declare-fun r_representationof (Value Value) Value)
(declare-fun In_String (Value) Bool)
(declare-fun v_nth (Value Value) Value)
(declare-fun v_integer (Int) Value)
(declare-fun v_length (Value) Value)
(declare-fun v_ff () Value)
(declare-fun v_tt () Value)
(declare-fun Good_C (Value) Bool)
(declare-fun alphai (IVMap) (Array Int ValueOption))
(declare-fun betai ((Array Int ValueOption)) IVMap)
(declare-fun v_cempty () Value)
(declare-fun FiniteC ((Array Int ValueOption)) Bool)
(declare-fun v_dot (String Value) Value)
(declare-fun Good_E (Value) Bool)
(declare-fun alphas (SVMap) (Array String ValueOption))
(declare-fun v_has_field (String Value) Bool)
(declare-fun betas ((Array String ValueOption)) SVMap)
(declare-fun v_eempty () Value)
(declare-fun FiniteE ((Array String ValueOption)) Bool)
(declare-fun v_string (String) Value)
(declare-fun O_LE (Value Value) Value)
(declare-fun O_LT (Value Value) Value)
(declare-fun O_GT (Value Value) Value)
(declare-fun O_GE (Value Value) Value)
(declare-fun O_Or (Value Value) Value)
(declare-fun O_And (Value Value) Value)
(declare-fun O_Minus (Value) Value)
(declare-fun O_Not (Value) Value)
(declare-fun O_NE (Value Value) Value)
(declare-fun O_EQ (Value Value) Value)
(declare-fun O_Mult (Value Value) Value)
(declare-fun O_Sub (Value Value) Value)
(declare-fun O_Sum (Value Value) Value)
(declare-fun In_Integer (Value) Bool)
(declare-fun In_Boolean (Value) Bool)
(declare-fun v_boolean (Bool) Value)
(declare-fun v_null () Value)
(declare-fun Good_R (Value) Bool)
(declare-fun v_has_field (String Value) Bool)
(declare-fun v_dot (String Value) Value)
(declare-fun |#55| () Value)
(declare-fun Good_E (Value) Bool)
(declare-fun v_tt () Value)
(declare-fun O_EQ (Value Value) Value)
(declare-fun request () Value)
(declare-fun In_String (Value) Bool)
(declare-fun v_boolean (Bool) Value)
(declare-fun maze () Value)
(declare-fun Good_R (Value) Bool)
(declare-fun In_Integer (Value) Bool)
(declare-fun mazeRep () Value)
(declare-fun v_nth (Value Value) Value)
(declare-fun v_integer (Int) Value)
(declare-fun Good_C (Value) Bool)
(declare-fun v_null () Value)
(declare-fun room () Value)
(declare-fun root () Value)
(declare-fun door () Value)
(declare-fun toRoom () Value)
(declare-fun v_ff () Value)
(assert (let ((a!1 (forall ((b Bool))
             (! (= (v_boolean b) (G (G_Boolean b))) :pattern ((v_boolean b)))))
      (a!2 (forall ((i Int))
             (! (= (v_integer i) (G (G_Integer i))) :pattern ((v_integer i)))))
      (a!3 (forall ((s String))
             (! (= (v_string s) (G (G_String s))) :pattern ((v_string s)))))
      (a!4 (forall ((v Value))
             (! (= (In_Boolean v) (and (is-G v) (is-G_Boolean (out_G v))))
                :pattern ((In_Boolean v)))))
      (a!5 (forall ((v Value))
             (! (= (In_Integer v) (and (is-G v) (is-G_Integer (out_G v))))
                :pattern ((In_Integer v)))))
      (a!6 (forall ((v Value))
             (! (= (In_String v) (and (is-G v) (is-G_String (out_G v))))
                :pattern ((In_String v)))))
      (a!7 (forall ((v1 Value) (v2 Value))
             (! (= (O_EQ v1 v2) (ite (= v1 v2) v_tt v_ff))
                :pattern ((O_EQ v1 v2)))))
      (a!8 (forall ((v1 Value) (v2 Value))
             (! (= (O_NE v1 v2) (ite (= v1 v2) v_ff v_tt))
                :pattern ((O_NE v1 v2)))))
      (a!9 (forall ((v Value))
             (! (= (O_Not v) (ite (not (= v v_tt)) v_tt v_ff))
                :pattern ((O_Not v)))))
      (a!10 (forall ((v1 Value) (v2 Value))
              (! (= (O_And v1 v2) (ite (and (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
                 :pattern ((O_And v1 v2)))))
      (a!11 (forall ((v1 Value) (v2 Value))
              (! (= (O_Or v1 v2) (ite (or (= v1 v_tt) (= v2 v_tt)) v_tt v_ff))
                 :pattern ((O_Or v1 v2)))))
      (a!12 (forall ((v Value))
              (! (let ((a!1 (= (str.len (of_G_String (out_G v)))
                               (of_G_Integer (out_G (v_length v))))))
                   (=> (and (is-G v) (is-G_String (out_G v))) a!1))
                 :pattern ((v_length v)))))
      (a!13 (forall ((v1 Value) (v2 Value))
              (! (let ((a!1 (ite (str.contains (of_G_String (out_G v1))
                                               (of_G_String (out_G v2)))
                                 v_tt
                                 v_ff)))
                   (=> (and (is-G v1)
                            (is-G_String (out_G v1))
                            (is-G v2)
                            (is-G_String (out_G v2)))
                       (= (v_contains v1 v2) a!1)))
                 :pattern ((v_contains v1 v2)))))
      (a!14 (forall ((v Value) (i Int))
              (! (let ((a!1 (v_string (str.at (of_G_String (out_G v)) i))))
                   (=> (and (is-G v) (is-G_String (out_G v)))
                       (= (v_nth v (v_integer i)) a!1)))
                 :pattern ((v_nth v (v_integer i))))))
      (a!15 (forall ((am (Array String ValueOption)))
              (=> (FiniteE am) (= (alphas (betas am)) am))))
      (a!16 (forall ((svm SVMap))
              (and (FiniteE (alphas svm)) (= (betas (alphas svm)) svm))))
      (a!17 (forall ((svm (Array String ValueOption)))
              (! (= (FiniteE svm) (= (default svm) NoValue))
                 :pattern ((FiniteE svm)))))
      (a!18 (= v_eempty
               (E (betas ((as const (Array String ValueOption)) NoValue)))))
      (a!19 (forall ((l String) (svm SVMap))
              (! (let ((a!1 (not (= (select (alphas svm) l) NoValue))))
                   (= (v_has_field l (E svm)) a!1))
                 :pattern ((v_has_field l (E svm))))))
      (a!20 (forall ((l String) (svm SVMap))
              (! (= (v_dot l (E svm)) (of_SomeValue (select (alphas svm) l)))
                 :pattern ((Good_E (E svm)) (v_dot l (E svm))))))
      (a!21 (forall ((am (Array Int ValueOption)))
              (=> (FiniteC am) (= (alphai (betai am)) am))))
      (a!22 (forall ((ivm IVMap))
              (and (FiniteC (alphai ivm)) (= (betai (alphai ivm)) ivm))))
      (a!23 (forall ((ivm (Array Int ValueOption)))
              (! (= (FiniteC ivm) (= (default ivm) NoValue))
                 :pattern ((FiniteC ivm)))))
      (a!24 (= v_cempty
               (C (betai ((as const (Array Int ValueOption)) NoValue)))))
      (a!25 (forall ((v Value) (i Int))
              (! (let ((a!1 (of_SomeValue (select (alphai (out_C v)) i))))
                   (=> (Good_C v) (= (v_nth v (v_integer i)) a!1)))
                 :pattern ((Good_C v) (v_nth v (v_integer i))))))
      (a!26 (forall ((v1 Value) (v2 Value))
              (! (let ((a!1 (exists ((i Int))
                              (let ((a!1 (< i
                                            (of_G_Integer (out_G (v_length v1))))))
                                (and (<= 0 i)
                                     a!1
                                     (= (v_nth v1 (v_integer i)) v2))))))
                   (=> (and (is-C v1))
                       (= (v_contains v1 v2) (ite a!1 v_tt v_ff))))
                 :pattern ((v_contains v1 v2)))))
      (a!27 (forall ((v Value))
              (! (=> (is-R v)
                     (and (is-C (representations v)) (is-C (representations v))))
                 :pattern ((is-R v)))))
      (a!28 (forall ((v Value) (r Value))
              (! (=> (is-R r)
                     (= (r_representationof v r)
                        (v_contains (representations r) v)))
                 :pattern ((r_representationof v r)))))
      (a!29 (forall ((v Value) (r Value))
              (! (=> (is-R r)
                     (= (r_resourceidof v r) (v_contains (identifiers r) v)))
                 :pattern ((r_resourceidof v r))))))
  (and (forall ((v Value)) (! (= (Good_C v) (is-C v)) :pattern ((Good_C v))))
       (forall ((v Value)) (! (= (Good_E v) (is-E v)) :pattern ((Good_E v))))
       (forall ((v Value)) (! (= (Good_R v) (is-R v)) :pattern ((Good_R v))))
       (= v_tt (G (G_Boolean true)))
       (= v_ff (G (G_Boolean false)))
       (= v_null (G G_Null))
       a!1
       a!2
       a!3
       a!4
       a!5
       a!6
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (+ (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Sum v1 v2) a!1))
            :pattern ((O_Sum v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (- (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Sub v1 v2) a!1))
            :pattern ((O_Sub v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (v_integer (* (of_G_Integer (out_G v1))
                                     (of_G_Integer (out_G v2))))))
              (= (O_Mult v1 v2) a!1))
            :pattern ((O_Mult v1 v2))))
       a!7
       a!8
       a!9
       (forall ((v Value))
         (! (let ((a!1 (v_integer (- (of_G_Integer (out_G v))))))
              (= (O_Minus v) a!1))
            :pattern ((O_Minus v))))
       a!10
       a!11
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (>= (of_G_Integer (out_G v1))
                                (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_GE v1 v2) a!1))
            :pattern ((O_GE v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (> (of_G_Integer (out_G v1))
                               (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_GT v1 v2) a!1))
            :pattern ((O_GT v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (< (of_G_Integer (out_G v1))
                               (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_LT v1 v2) a!1))
            :pattern ((O_LT v1 v2))))
       (forall ((v1 Value) (v2 Value))
         (! (let ((a!1 (ite (<= (of_G_Integer (out_G v1))
                                (of_G_Integer (out_G v2)))
                            v_tt
                            v_ff)))
              (= (O_LE v1 v2) a!1))
            :pattern ((O_LE v1 v2))))
       a!12
       a!13
       a!14
       a!15
       a!16
       a!17
       (forall ((v Value))
         (! (let ((a!1 (and (is-E v) (FiniteE (alphas (out_E v))))))
              (= (Good_E v) a!1))
            :pattern ((Good_E v))))
       a!18
       a!19
       a!20
       a!21
       a!22
       a!23
       (forall ((v Value))
         (! (let ((a!1 (and (is-C v) (FiniteC (alphai (out_C v))))))
              (= (Good_C v) a!1))
            :pattern ((Good_C v))))
       (forall ((v Value))
         (! (let ((a!1 (>= (of_G_Integer (out_G (v_length v))) 0)))
              (=> (Good_C v) a!1))
            :pattern ((Good_C v))))
       (forall ((v Value))
         (! (let ((a!1 (forall ((i Int))
                         (let ((a!1 (< i (of_G_Integer (out_G (v_length v)))))
                               (a!2 (is-SomeValue (select (alphai (out_C v)) i))))
                           (=> (and (<= 0 i) a!1) a!2)))))
              (= (Good_C v) a!1))
            :pattern ((Good_C v))))
       a!24
       a!25
       a!26
       a!27
       (forall ((v Value))
         (let ((a!1 (forall ((i Int))
                      (let ((a!1 (of_G_Integer (out_G (v_length (representations v)))))
                            (a!2 (not (is-R (v_nth (representations v)
                                                   (v_integer i))))))
                        (=> (and (< 0 i) (< i a!1)) (and a!2))))))
           (=> (is-R v) a!1)))
       (forall ((v Value))
         (let ((a!1 (forall ((i Int))
                      (let ((a!1 (of_G_Integer (out_G (v_length (identifiers v)))))
                            (a!2 (and (In_String (v_nth (identifiers v)
                                                        (v_integer i))))))
                        (=> (and (< 0 i) (< i a!1)) a!2)))))
           (=> (is-R v) a!1)))
       a!28
       a!29)))
(assert (let ((a!1 (of_G_String (out_G (v_dot "name" (v_dot "body" request)))))
      (a!2 (re.union (re.union (re.union (re.range "a" "z") (re.range "A" "Z"))
                               (re.range "0" "9"))
                     (re.union (re.range " " " ")
                               (re.union (re.range "\x09" "\x09")
                                         (re.range "\n" "\n")))))
      (a!5 (v_boolean (and (Good_E (v_dot "template" request)))))
      (a!6 (and (Good_C (v_dot "start" (v_dot "_links" mazeRep)))
                (forall ((|\|#29\|| Int))
                  (let ((a!1 (Good_E (v_nth (v_dot "start"
                                                   (v_dot "_links" mazeRep))
                                            (v_integer |\|#29\||))))
                        (a!2 (v_has_field "href"
                                          (v_nth (v_dot "start"
                                                        (v_dot "_links" mazeRep))
                                                 (v_integer |\|#29\||))))
                        (a!3 (v_dot "href"
                                    (v_nth (v_dot "start"
                                                  (v_dot "_links" mazeRep))
                                           (v_integer |\|#29\||)))))
                    (and a!1 a!2 (In_String a!3))))))
      (a!8 (In_String (v_dot "href" (v_dot "self" (v_dot "_links" mazeRep)))))
      (a!9 (forall ((|\|#30\|| Int))
             (let ((a!1 (Good_E (v_nth (v_dot "orphanedRooms"
                                              (v_dot "_embedded" mazeRep))
                                       (v_integer |\|#30\||))))
                   (a!2 (v_has_field "_links"
                                     (v_nth (v_dot "orphanedRooms"
                                                   (v_dot "_embedded" mazeRep))
                                            (v_integer |\|#30\||))))
                   (a!3 (v_dot "_links"
                               (v_nth (v_dot "orphanedRooms"
                                             (v_dot "_embedded" mazeRep))
                                      (v_integer |\|#30\||))))
                   (a!4 (v_has_field "name"
                                     (v_nth (v_dot "orphanedRooms"
                                                   (v_dot "_embedded" mazeRep))
                                            (v_integer |\|#30\||))))
                   (a!5 (v_dot "name"
                               (v_nth (v_dot "orphanedRooms"
                                             (v_dot "_embedded" mazeRep))
                                      (v_integer |\|#30\||))))
                   (a!6 (v_has_field "id"
                                     (v_nth (v_dot "orphanedRooms"
                                                   (v_dot "_embedded" mazeRep))
                                            (v_integer |\|#30\||))))
                   (a!7 (v_dot "id"
                               (v_nth (v_dot "orphanedRooms"
                                             (v_dot "_embedded" mazeRep))
                                      (v_integer |\|#30\||)))))
               (and a!1
                    a!2
                    (Good_E a!3)
                    (v_has_field "doors" a!3)
                    (Good_E (v_dot "doors" a!3))
                    (v_has_field "href" (v_dot "doors" a!3))
                    (In_String (v_dot "href" (v_dot "doors" a!3)))
                    (v_has_field "self" a!3)
                    (Good_E (v_dot "self" a!3))
                    (v_has_field "href" (v_dot "self" a!3))
                    (In_String (v_dot "href" (v_dot "self" a!3)))
                    (v_has_field "maze" a!3)
                    (Good_E (v_dot "maze" a!3))
                    (v_has_field "href" (v_dot "maze" a!3))
                    (In_String (v_dot "href" (v_dot "maze" a!3)))
                    a!4
                    (In_String a!5)
                    a!6
                    (In_Integer a!7)))))
      (a!10 (v_boolean (and (Good_E (v_dot "template" |#55|))))))
(let ((a!3 (and (In_String (v_dot "name" (v_dot "body" request)))
                (str.in.re a!1 ((_ re.loop 3 50) a!2))))
      (a!7 (or a!6 (= (v_dot "start" (v_dot "_links" mazeRep)) v_null))))
(let ((a!4 (and (Good_E (v_dot "body" request))
                (v_has_field "name" (v_dot "body" request))
                (In_String (v_dot "name" (v_dot "body" request)))
                (= (ite a!3 v_tt v_ff) v_tt))))
(let ((a!11 (and true
                 (= (v_boolean a!4) v_tt)
                 (Good_R toRoom)
                 (= (type toRoom) "Room")
                 (Good_R door)
                 (= (type door) "Door")
                 (In_String root)
                 (Good_R room)
                 (= (type room) "Room")
                 (Good_E request)
                 (v_has_field "template" request)
                 true
                 (= a!5 v_tt)
                 (v_has_field "header" request)
                 (Good_E (v_dot "header" request))
                 (v_has_field "location" request)
                 (In_String (v_dot "location" request))
                 (v_has_field "body" request)
                 true
                 (Good_E mazeRep)
                 (v_has_field "_links" mazeRep)
                 (Good_E (v_dot "_links" mazeRep))
                 (v_has_field "start" (v_dot "_links" mazeRep))
                 a!7
                 (v_has_field "self" (v_dot "_links" mazeRep))
                 (Good_E (v_dot "self" (v_dot "_links" mazeRep)))
                 (v_has_field "href" (v_dot "self" (v_dot "_links" mazeRep)))
                 a!8
                 (v_has_field "_embedded" mazeRep)
                 (Good_E (v_dot "_embedded" mazeRep))
                 (v_has_field "orphanedRooms" (v_dot "_embedded" mazeRep))
                 (Good_C (v_dot "orphanedRooms" (v_dot "_embedded" mazeRep)))
                 a!9
                 (v_has_field "name" mazeRep)
                 (In_String (v_dot "name" mazeRep))
                 (v_has_field "id" mazeRep)
                 (In_Integer (v_dot "id" mazeRep))
                 (Good_R maze)
                 (= (type maze) "Maze")
                 (Good_E |#55|)
                 (v_has_field "template" |#55|)
                 true
                 (= a!10 v_tt)
                 (v_has_field "header" |#55|)
                 (Good_E (v_dot "header" |#55|))
                 (v_has_field "location" |#55|)
                 (In_String (v_dot "location" |#55|))
                 (v_has_field "body" |#55|)
                 true
                 (= (O_EQ |#55| request) v_tt)
                 (= (O_EQ |#55| request) v_tt))))
(let ((a!12 (=> a!11
                (and (Good_E |#55|)
                     (v_has_field "body" |#55|)
                     (Good_E (v_dot "body" |#55|))
                     (v_has_field "name" (v_dot "body" |#55|))
                     true))))
  (not a!12)))))))

Curiously, if I try using the Java API parse from that file (after removing the duplicated lines generated by solver.toString() and removing the (check-sat)):

solver.reset();
String code = FileUtils.readFileToString(new File("<path to file>.z3"), Charset.defaultCharset());
BoolExpr assertions = context.parseSMTLIB2String(code, null, null, null, null);
solver.add(assertions);
solver.check();

The Java API returns unsat correctly. So, my question is, why is that after creating the assertions using the Java API and checking if satisfiable it returns unknown but using the commandline-tool/parsing it returns unsat correctly?

Thanks.

[daparpon]

I have exactly the same problem (briefly reported in Issue #1097). I subscribe myself to this Issue since I am also interested in the answer.

[wintersteiger]

What kind of solver are you using, i.e. how did you get your solver object?

[facferreira]

Simply by doing context.mkSolver(); (The context was created with an empty map)

[NikolajBjorner]

to properly repro this one would need a log (Z3_open_log before any context is created) or a java version.

[alcides]

Hi, I am facing the same issue (working on the same project).

I am compiling a test to reveal 3 different errors related to Java bindings. This is the first one, in which two different SMT2 models (generated by the Java bindings) both have inconsistent behaviours:

Test consists on loading the smt2 model, and checking for sat. No defaults are set.

Java Bindings: unknown Python z3: unsat z3 command-line: unsat

I am providing everything to reproduce the problem in the following repo, including how to generate the models, the output in both MacOS and Linux of the different bindings, and the outputs/$os_execution/$file_model.log resulted from using z3's openlog.

https://github.com/alcides/z3test (Problem 2 in the Readme.md)

[alcides]

Any update on this issue? This is preventing us from working on this project, not being able to trust the z3 Java bindings.

[daparpon]

Same here. Our project is in standby, waiting for this issue with Z3 to be solved...

[NikolajBjorner]

Is it possible to get a "z3.log" file from the Java interaction and the python interaction as well? The API for creating a log file is called Z3_open_log and there are Java versions of this (from Python just invoke z3.Z3_open_log directly). I assume you are using Z3 from a single thread as the logging features are not supported for multiple threads.

This would make it possible to debug the "unknown" vs. "unsat" behavior. The python and Java behavior should be similar, the only exception is the order in which expressions are built. You can emulate checking different expression orders by setting the parameter smt.random_seed to different values and check if the solver returns alternations of "unknown" vs. "unsat".

[alcides]

Here you have the two logs of one such example:

https://github.com/alcides/z3test/blob/master/linux.smt2_python.log

https://github.com/alcides/z3test/blob/master/linux.smt2_java.log

[NikolajBjorner]

And they provide different answers (unsat vs. unknown)? Seem they were generated for 4.6.0 and not current 4.6.1.

[alcides]

Yes, they do. On 3 different (but somehow similar) smt2 models.

I used commit 1323b8f63f21f40b7a264140ff84afa3dad989c8, which i believe its close to 4.6.1. I'll run with the newest version, but I believe the problem remains.

[alcides]

The same behaviour occurs with small.smt2.

macos.smt2 and linux.smt2 now fail to parse on command-line z3 and python bindings with the latest z3 version. Java still gives unknown on both examples.

Despite the version strings, it was executed with all bindings compiled from the commit fbbc57168d8e66979bf61ff4cfa355f9351d98c8.

OS: Darwin x86_64
--------- Java version --------- 
Z3 Full Version String: Z3 4.6.0.0
--------  Python version ------- 
Z3 4.6.1.7919 master z3-4.6.0-143-gfbbc5716
-----  Command-line version ----- 
Z3 version 4.6.1 - 64 bit
--------------------------
Model: linux.smt2
cmline: (error "line 63 column 46: unknown function/constant is-G")
unsat 
(error "line 63 column 46: unknown function/constant is-G")
Traceback (most recent call last):
  File "t.py", line 10, in <module>
    s.from_file(fname)
  File "/usr/local/lib/python2.7/site-packages/z3/z3.py", line 6333, in from_file
    _handle_parse_error(e, self.ctx)
  File "/usr/local/lib/python2.7/site-packages/z3/z3.py", line 8104, in _handle_parse_error
    raise ex
z3.z3types.Z3Exception: parser error
WARNING: an assumption must be a propositional variable or the negation of one
java: UNKNOWN
java reason: unknown
--------------------------
Model: macos.smt2
cmline: (error "line 62 column 46: unknown function/constant is-G")
sat 
(error "line 62 column 46: unknown function/constant is-G")
Traceback (most recent call last):
  File "t.py", line 10, in <module>
    s.from_file(fname)
  File "/usr/local/lib/python2.7/site-packages/z3/z3.py", line 6333, in from_file
    _handle_parse_error(e, self.ctx)
  File "/usr/local/lib/python2.7/site-packages/z3/z3.py", line 8104, in _handle_parse_error
    raise ex
z3.z3types.Z3Exception: parser error
WARNING: an assumption must be a propositional variable or the negation of one
java: UNKNOWN
java reason: unknown
--------------------------
Model: small.smt2
cmline: unsat 
python: unsat
WARNING: an assumption must be a propositional variable or the negation of one
java: UNKNOWN
java reason: unknown

[NikolajBjorner]

The version string in the log files should be along the lines of: V "4.6.1.0 Feb 27 2018"

I am unable to run your logs using the current master. Sometimes Java installations have been seen picking up stale versions of libz3.dll

[alcides]

I am now running this version: https://github.com/Z3Prover/bin/commit/b6ffdb1fbceaaf01da6d2b6ca0b1071caf8aa87f

It seems that SIP on MacOS prevents -Djava.library.path from ever being used (https://github.com/Z3Prover/z3/issues/294). Unfortunately Apple does not fix this issues, but there should be a clear warning in the z3 documentation that dylibs should be in the current path on MacOS.

However, using the same version, Java still produces unknown while Python produces unsat.

The new logs are available here:

https://github.com/alcides/z3test/blob/master/small.smt2_java.log https://github.com/alcides/z3test/blob/master/small.smt2_python.log

[NikolajBjorner]

The Java trace triggered some debug asserts that I have taken care of now, but they should be benign. For these two traces the calls into the APIs are different.

For Java: 3:Z3_mk_config 5:Z3_set_param_value 7:Z3_mk_context_rc 4:Z3_del_config 328:Z3_set_ast_print_mode 338:Z3_get_error_code 335:Z3_parse_smtlib2_string 338:Z3_get_error_code 255:Z3_get_ast_kind 338:Z3_get_error_code 252:Z3_get_sort 338:Z3_get_error_code 207:Z3_get_sort_kind 338:Z3_get_error_code 258:Z3_is_algebraic_number 338:Z3_get_error_code 257:Z3_is_numeral_ast 338:Z3_get_error_code 256:Z3_is_app 338:Z3_get_error_code 9:Z3_inc_ref 338:Z3_get_error_code 407:Z3_mk_solver 338:Z3_get_error_code 415:Z3_solver_inc_ref 338:Z3_get_error_code 427:Z3_solver_check_assumptions 338:Z3_get_error_code 433:Z3_solver_get_reason_unknown 338:Z3_get_error_code

For Python: 3:Z3_mk_config 7:Z3_mk_context_rc 338:Z3_get_error_code 328:Z3_set_ast_print_mode 338:Z3_get_error_code 4:Z3_del_config 407:Z3_mk_solver 338:Z3_get_error_code 415:Z3_solver_inc_ref 338:Z3_get_error_code 424:Z3_solver_from_file 338:Z3_get_error_code 427:Z3_solver_check_assumptions 338:Z3_get_error_code

(I get this by rerunning the logs and then tracing -tr:z3_replayer_cmd)

The Java version calls the parse_smtlib2_string function. The Python version calls solver_from_string, which loads assertions into the solver object. The Java trace never adds the assertions to the solver, so the solver call is trivial.

[alcides]

I fixed this issue, calling Solver.fromFile()

In retrospective, I believe this was the result from unclear Java bindings documentation. I will try to improve it, if I find the time.

You can close this.

[NikolajBjorner]

So if I write:

/**
 * Parse the given string using the SMT-LIB2 parser. 
 * 
 * @return A conjunction of assertions.
 *         If the string contains push/pop commands, the
 *         set of assertions returned are the ones in the 
 *         last scope level.
 **/