z3py: How to improve the time efficiency of the following code

Question

This is a simplified code using the similar implementation idea as the z3py code for another problem I am trying to solve which is more complex and takes about 1 minute to run.

The intuition of the following code is to translate the array of integers in the inputArray into the array of months defined as EnumSort, which is essentially to infer the model of monthArray.

from z3 import *
s = Solver()

Month,(Jan,Feb,Mar,Apr,May,Jun,Jul,Aug,Sep,Oct,Nov,Dec)=EnumSort('Month',['Jan','Feb','Mar','Apr','May','Jun','Jul','Aug','Sep','Oct','Nov','Dec'])
monthArray = Array('monthArray',IntSort(), Month)
inputArray = Array('inputArray',IntSort(),IntSort())
tempArray = Array('tempArray',IntSort(),IntSort())

intArray = [1,3,6,7,8,3,5,6,3,12,11,5,2,5,7,3,7,3,2,7,12,4,5,1,10,9]
for idx,num in enumerate(intArray):
    tempArray = Store(tempArray,idx,num)

s.add(inputArray==tempArray)

length = Int('length')
s.add(length == len(intArray))
i = Int('i')
s.add(ForAll(i,Implies(And(i>=0,i<length),And(
    Implies(inputArray[i]==1,monthArray[i]==Jan),
    Implies(inputArray[i]==2,monthArray[i]==Feb),
    Implies(inputArray[i]==3,monthArray[i]==Mar),
    Implies(inputArray[i]==4,monthArray[i]==Apr),
    Implies(inputArray[i]==5,monthArray[i]==May),
    Implies(inputArray[i]==6,monthArray[i]==Jun),
    Implies(inputArray[i]==7,monthArray[i]==Jul),
    Implies(inputArray[i]==8,monthArray[i]==Aug),
    Implies(inputArray[i]==9,monthArray[i]==Sep),
    Implies(inputArray[i]==10,monthArray[i]==Oct),
    Implies(inputArray[i]==11,monthArray[i]==Nov),
    Implies(inputArray[i]==12,monthArray[i]==Dec)
    ))))

print s.check()
print s.model()

Could anyone give me some suggestions about the ways to improve the time efficiency using this code as an example? Thanks.

Edit: SMT language output by calling Solver.to_smt2()

(set-info :status unknown)
(declare-datatypes () ((Month (Jan ) (Feb ) (Mar ) (Apr ) (May ) (Jun ) (Jul ) (Aug ) (Sep ) (Oct ) (Nov ) (Dec ))))
(declare-fun inputArray () (Array Int Int))
(declare-fun length () Int)
(declare-fun monthArray () (Array Int Month))
(assert
(= (select inputArray 0) 1))
(assert
(= (select inputArray 1) 3))
(assert
(= (select inputArray 2) 6))
(assert
(= (select inputArray 3) 7))
(assert
(= (select inputArray 4) 8))
(assert
(= (select inputArray 5) 3))
(assert
(= (select inputArray 6) 5))
(assert
(= (select inputArray 7) 6))
(assert
(= (select inputArray 8) 3))
(assert
(= (select inputArray 9) 12))
(assert
(= (select inputArray 10) 11))
(assert
(= (select inputArray 11) 5))
(assert
(= (select inputArray 12) 2))
(assert
(= (select inputArray 13) 5))
(assert
(= (select inputArray 14) 7))
(assert
(= (select inputArray 15) 3))
(assert
(= (select inputArray 16) 7))
(assert
(= (select inputArray 17) 3))
(assert
(= (select inputArray 18) 2))
(assert
(= (select inputArray 19) 7))
(assert
(= (select inputArray 20) 12))
(assert
(= (select inputArray 21) 4))
(assert
(= (select inputArray 22) 5))
(assert
(= (select inputArray 23) 1))
(assert
(= (select inputArray 24) 10))
(assert
(= (select inputArray 25) 9))
(assert
(= length 26))
(assert
(forall ((i Int) )(let (($x172 (=> (= (select inputArray i) 12) (= (select monthArray i) Dec))))
(let (($x175 (=> (= (select inputArray i) 11) (= (select monthArray i) Nov))))
(let (($x178 (=> (= (select inputArray i) 10) (= (select monthArray i) Oct))))
(let (($x181 (=> (= (select inputArray i) 9) (= (select monthArray i) Sep))))
(let (($x184 (=> (= (select inputArray i) 8) (= (select monthArray i) Aug))))
(let (($x187 (=> (= (select inputArray i) 7) (= (select monthArray i) Jul))))
(let (($x190 (=> (= (select inputArray i) 6) (= (select monthArray i) Jun))))
(let (($x193 (=> (= (select inputArray i) 5) (= (select monthArray i) May))))
(let (($x196 (=> (= (select inputArray i) 4) (= (select monthArray i) Apr))))
(let (($x199 (=> (= (select inputArray i) 3) (= (select monthArray i) Mar))))
(let (($x202 (=> (= (select inputArray i) 2) (= (select monthArray i) Feb))))
(let (($x205 (=> (= (select inputArray i) 1) (= (select monthArray i) Jan))))
(=> (and (>= i 0) (< i length)) (and $x205 $x202 $x199 $x196 $x193 $x190 $x187 $x184 $x181 $x178 $x175 $x172)))))))))))))))
)
(check-sat)

Answer 1

I find using 'qflia' (quantifier-free linear integer arithmetic) solver, instead of the general solver 'Solver()', improve the efficiency by about 3x in my case.