Failure of tests on fresh checkout (Mac OS X)

[wbl]

I've just started to get this running, and run into a roadblock:

$pip3.7 show z3-solver Name: z3-solver Version: 4.8.7.0 Summary: an efficient SMT solver library Home-page: https://github.com/Z3Prover/z3 Author: The Z3 Theorem Prover Project Author-email: None License: MIT License Location: /usr/local/lib/python3.7/site-packages Requires: Required-by: `$python3 runAutoGroup.py --sdl schemes/cl04.sdl --config schemes/configCL.py -o TestCL -v runAutoGroup.py:3: DeprecationWarning: the imp module is deprecated in favour of importlib; see the module's documentation for alternative uses import imp runAutoGroup.py:792: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead startTime = time.clock() sdl: 1 name := LRSW sdl: 2 setting := symmetric sdl: 3 sdl: 4 BEGIN :: types sdl: 5 x := ZR sdl: 6 y := ZR sdl: 7 z := ZR sdl: 8 END :: types sdl: 9 sdl: 10 sdl: 11 BEGIN :: func:setup sdl: 12 input := None sdl: 13 x := random(ZR) sdl: 14 y := random(ZR) sdl: 15 sdl: 16 g := random(G1) sdl: 17 sdl: 18 assumpKey := list{g, x, y} sdl: 19 sdl: 20 output := assumpKey sdl: 21 END :: func:setup sdl: 22 sdl: 23 sdl: 24 BEGIN :: func:assump sdl: 25 input := assumpKey sdl: 26 assumpKey := expand{g, x, y} sdl: 27 X := (g^x) sdl: 28 Y := (g^y) sdl: 29 sdl: 30 assumpVar := list{X, Y} sdl: 31 sdl: 32 output := assumpVar sdl: 33 END :: func:assump reducing size of 'signature' <=== Assumption Instance Graph ===> digraph assumption { g -> Y g -> X g }

<=== Assumption Instance Graph ===> 16 : G1 :=> g := random(G1) , loop :=> False

runAutoGroup.py:794: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead endTime = time.clock() ['reductionCL'] runAutoGroup.py:820: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead startTime = time.clock() sdl: 1 name := cl04 sdl: 2 setting := symmetric sdl: 3 sdl: 4 BEGIN :: types sdl: 5 m := ZR sdl: 6 END :: types sdl: 7 sdl: 8 BEGIN :: func:setup sdl: 9 input := list{assumpKey, assumpVar} sdl: 10 sdl: 11 sdl: 12 x := random(ZR) sdl: 13 y := random(ZR) sdl: 14 g := random(G1) sdl: 15 sdl: 16 X := (g^x) sdl: 17 Y := (g^y) sdl: 18 sdl: 19 reductionKey := list{x, y} sdl: 20 reductionParams := list{p, g, X, Y} sdl: 21 output := list{reductionKey, reductionParams} sdl: 22 END :: func:setup sdl: 23 sdl: 24 sdl: 25 BEGIN :: func:queries sdl: 26 input := list{m, reductionParams, reductionKey} sdl: 27 reductionKey := expand{x, y} sdl: 28 reductionParams := expand{p, g, X, Y} sdl: 29 sdl: 30 r := random(ZR) sdl: 31 a := (g^r) sdl: 32 b := (a^y) sdl: 33 c := (a^(x + ((m * x) * y))) sdl: 34 sdl: 35 sig := list{a, b, c} sdl: 36 sdl: 37 output := sig sdl: 38 END :: func:queries sdl: 39 sdl: 40 reducing size of 'signature' <=== Reduction Setup Graph ===> digraph setup { g g -> X g -> Y }

<=== Reduction Setup Graph ===> <=== Reduction Query Graph (backward) ===> digraph queries { g -> a a -> b a -> c }

<=== Reduction Query Graph (backward) ===> <=== Reduction Graph ===> digraph reduction { g -> Y a -> c a -> b g g -> a g -> X }

<=== Reduction Graph ===> 14 : G1 :=> g := random(G1) , loop :=> False runAutoGroup.py:822: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead endTime = time.clock() runAutoGroup.py:870: DeprecationWarning: time.clock has been deprecated in Python 3.3 and will be removed from Python 3.8: use time.perf_counter or time.process_time instead startTime = time.clock() sdl: 1 name := cl04 sdl: 2 setting := symmetric sdl: 3 sdl: 4 BEGIN :: types sdl: 5 M := Str sdl: 6 END :: types sdl: 7 sdl: 8 BEGIN :: func:setup sdl: 9 input := list{None} sdl: 10 g := random(G1) sdl: 11 output := g sdl: 12 END :: func:setup sdl: 13 sdl: 14 sdl: 15 BEGIN :: func:keygen sdl: 16 input := list{g} sdl: 17 x := random(ZR) sdl: 18 y := random(ZR) sdl: 19 X := (g^x) sdl: 20 Y := (g^y) sdl: 21 sk := list{x, y} sdl: 22 pk := list{X, Y} sdl: 23 output := list{pk, sk} sdl: 24 END :: func:keygen sdl: 25 sdl: 26 sdl: 27 BEGIN :: func:sign sdl: 28 input := list{g, sk, M} sdl: 29 sk := expand{x, y} sdl: 30 r := random(ZR) sdl: 31 m := H(M,ZR) sdl: 32 a := (g^r) sdl: 33 b := (a^y) sdl: 34 c := (a^(x + ((m * x) * y))) sdl: 35 sig := list{a, b, c} sdl: 36 output := sig sdl: 37 END :: func:sign sdl: 38 sdl: 39 sdl: 40 BEGIN :: func:verify sdl: 41 input := list{pk, g, M, sig} sdl: 42 sig := expand{a, b, c} sdl: 43 pk := expand{X, Y} sdl: 44 m := H(M,ZR) sdl: 45 BEGIN :: if sdl: 46 if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}} sdl: 47 output := True sdl: 48 else sdl: 49 output := False sdl: 50 END :: if sdl: 51 END :: func:verify sdl: 52 name is cl04 setting is symmetric reducing size of 'signature' 10 : G1 :=> g := random(G1) , loop :=> False Each: if {{e(a,Y) == e(g,b)} and {(e(X,a) * (e(X,b)^m)) == e(g,c)}} <=== Setup Graph ===> digraph setup { }

<=== Setup Graph ===> <=== Keygen Graph ===> digraph keygen { g -> X g -> Y }

<=== Keygen Graph ===> <=== Sign Graph ===> digraph sign { g -> a a -> b a -> c }

<=== Sign Graph ===> <=== Verify Graph ===> digraph verify { a -> "P1[0]" Y -> "P1[1]" g -> "P2[0]" b -> "P2[1]" X -> "P3[0]" a -> "P3[1]" X -> "P4[0]" b -> "P4[1]" g -> "P5[0]" c -> "P5[1]" }

<=== Verify Graph ===> <=== Scheme Graph ===> digraph cl04 { g -> Y a -> c a -> b X -> "P3[0]" g -> "P5[0]" a -> "P1[0]" a -> "P3[1]" X -> "P4[0]" Y -> "P1[1]" b -> "P4[1]" g -> a b -> "P2[1]" g -> X g -> "P2[0]" c -> "P5[1]" }

<=== Scheme Graph ===>

<=== Assumption Graph ===> digraph assumption { g -> Y g -> X g }

<=== Assumption Graph ===> <=== Reduction Graph ===> digraph reduction { g -> Y a -> c a -> b g g -> a g -> X }

<=== Reduction Graph ===> <=== Merged Graph ===> digraph merged { g -> Y a -> c a -> b X -> "P3[0]" g -> "P5[0]" a -> "P1[0]" a -> "P3[1]" g X -> "P4[0]" Y -> "P1[1]" b -> "P4[1]" g -> a b -> "P2[1]" g -> X g -> "P2[0]" c -> "P5[1]" }

<=== Merged Graph ===> pair vars LHS: ['a', 'g', 'X', 'X', 'g'] pair vars RHS: ['Y', 'b', 'a', 'b', 'c'] list of gens : ['g'] constraintList: [] pruned varList: ['a', 'b', 'c'] <===== Instantiate Z3 solver =====> Traceback (most recent call last): File "runAutoGroup.py", line 891, in configAutoGroup(dest_path, sdl_file, config_file, output_file, verbose, benchmarkOpt, estimateSize, short_option, run_auto_group) File "runAutoGroup.py", line 871, in configAutoGroup (outfile_scheme, outfile_assump) = runAutoGroup(sdl_file, cm, options, verbose, assumptionData, reductionData) File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 2461, in runAutoGroup fileSuffix, resultDict = searchForSolution(info, short, constraintList, txor, varTypes, config, generators) File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 898, in searchForSolution pkMapMin, pkListMin, assumpMapMin, assumpList, xorVarMap) File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/convertToAsymmetric.py", line 625, in instantiateZ3Solver (result, satisfiable) = solveUsingSMT(info, options, shortOpt, timeOpt) File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/solver.py", line 729, in solveUsingSMT (mySolver, Conditions, Values, EntireSet) = getNewSolver(clauses, Z3vars, hard_constraints) # add File "/Users/watsonladd/ext-repos/auto-tools/auto_group/src/solver.py", line 655, in getNewSolver if Z3vars.get(x) and Z3vars.get(y): File "/usr/local/lib/python3.7/site-packages/z3/z3.py", line 343, in bool raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.") z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values.`

Sadly installing trunk z3 didn't work with python3 on my machine, but I'm a bit surprised this would have changed. Let me know what information would help in digging into this more.