search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

infinite loop in modulo operation with variable divisor #7464

Open amigalemming opened 6 days ago

amigalemming commented 6 days ago

I have the following Liquid Haskell code:

module Example.BinaryGCD where

import Prelude hiding (even)

{-@
even ::
   n : Integer ->
   {m : Bool | m = (n mod 2 = 0)}
@-}
even :: Integer -> Bool
even n = mod n 2 == 0

{-@
divTwoPow ::
   nn : {n : Integer | n>0} ->
   {m : Integer | m>0 && m mod 2 = 1 && m <= nn && nn mod m = 0}
@-}
divTwoPow :: Integer -> Integer
divTwoPow n =
   if even n then divTwoPow (div n 2) else n

The nn mod m = 0 part sends Z3 (version 4.8.12) to an infinite loop. Here is the SMT code that Liquid Haskell extracts from the code above:

(set-option :auto-config false)
(set-option :model true)

(set-option :smt.mbqi false)

(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)
(define-sort LSet () (Array Elt Bool))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(define-fun smt_map_cup ((m1 Map) (m2 Map)) Map ((_ map (+ (Elt Elt) Elt)) m1 m2))
(define-fun smt_map_prj ((s LSet) (m Map)) Map ((_ map (ite (Bool Elt Elt) Elt)) s m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_to_set ((m Map)) LSet ((_ map (> (Elt Elt) Bool)) m ((as const (Array Elt Elt)) 0)))
(define-fun smt_map_max ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_min ((m1 Map) (m2 Map)) Map (lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i))))
(define-fun smt_map_shift ((n Int) (m Map)) Map (lambda ((i Int)) (select m (- i n))))
(define-fun smt_map_def ((v Elt)) Map ((as const (Map)) v))
(define-fun bool_to_int ((b Bool)) Int (ite b 1 0))
(define-fun Z3_OP_MUL ((x Int) (y Int)) Int (* x y))
(define-fun Z3_OP_DIV ((x Int) (y Int)) Int (div x y))
(declare-fun GHC.Internal.Float.log () Int)
(declare-fun GHC.Internal.Real.recip () Int)
(declare-fun GHC.Internal.Real.div () Int)
(declare-fun GHC.Types.LT () Int)
(declare-fun VV$35$$35$F$35$$35$10 () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ () Int)
(declare-fun GHC.Internal.Real.rem () Int)
(declare-fun GHC.Classes.$124$$124$ () Int)
(declare-fun GHC.Classes.min () Int)
(declare-fun GHC.Internal.Data.Tuple.snd () Int)
(declare-fun GHC.Internal.Real.$36$W$58$$37$ () Int)
(declare-fun GHC.Num.Integer.$36$fEqInteger () Int)
(declare-fun GHC.Internal.Enum.C$58$Bounded () Int)
(declare-fun snd () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun GHC.Internal.Base.. () Int)
(declare-fun GHC.Internal.Stack.Types.EmptyCallStack () Int)
(declare-fun GHC.Classes.$38$$38$ () Int)
(declare-fun GHC.Internal.Real.quotRem () Int)
(declare-fun VV$35$$35$F$35$$35$3 () Int)
(declare-fun GHC.Internal.Stack.Types.FreezeCallStack () Int)
(declare-fun VV$35$$35$F$35$$35$17 () Int)
(declare-fun len () Int)
(declare-fun VV$35$$35$F$35$$35$8 () Int)
(declare-fun GHC.Types.TrNameS () Int)
(declare-fun GHC.Classes.$61$$61$ () Int)
(declare-fun cast_as () Int)
(declare-fun Example.BinaryGCD.even () Int)
(declare-fun VV$35$$35$F$35$$35$12 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP () Int)
(declare-fun GHC.Internal.Float.asinh () Int)
(declare-fun GHC.Classes.$62$ () Int)
(declare-fun GHC.Internal.Float.asin () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO () Bool)
(declare-fun lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI () Int)
(declare-fun GHC.Internal.Real.quot () Int)
(declare-fun GHC.Types.Module () Int)
(declare-fun GHC.Internal.Base.map () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR () Int)
(declare-fun fst () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun papp2 () Int)
(declare-fun GHC.Internal.Num.abs () Int)
(declare-fun GHC.Num.Integer.IP () Int)
(declare-fun GHC.Internal.Real.$47$ () Int)
(declare-fun papp7 () Int)
(declare-fun papp1 () Int)
(declare-fun GHC.Internal.Float.sin () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805063$35$$35$d2YT () Int)
(declare-fun GHC.Internal.Float.$42$$42$ () Int)
(declare-fun GHC.Classes.compare () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN () Bool)
(declare-fun lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM () Int)
(declare-fun papp5 () Int)
(declare-fun GHC.Num.Integer.IN () Int)
(declare-fun papp4 () Int)
(declare-fun GHC.Internal.Num.negate () Int)
(declare-fun GHC.Internal.Base.$36$ () Int)
(declare-fun GHC.Types.False () Bool)
(declare-fun GHC.Internal.Float.acos () Int)
(declare-fun GHC.Internal.Base.$43$$43$ () Int)
(declare-fun GHC.Types.TrNameD () Int)
(declare-fun lit$36$Example.BinaryGCD () Str)
(declare-fun lit$36$htam$45$liquid$45$0.0$45$inplace () Str)
(declare-fun totalityError () Int)
(declare-fun GHC.Classes.$47$$61$ () Int)
(declare-fun GHC.Internal.Float.tanh () Int)
(declare-fun GHC.Internal.Real.divMod () Int)
(declare-fun GHC.Internal.Float.cosh () Int)
(declare-fun GHC.Internal.Float.logBase () Int)
(declare-fun GHC.Internal.Maybe.Just () Int)
(declare-fun VV$35$$35$F$35$$35$6 () Int)
(declare-fun Example.BinaryGCD.divTwoPow () Int)
(declare-fun GHC.Tuple.$40$$44$$41$ () Int)
(declare-fun GHC.Internal.Real.$58$$37$ () Int)
(declare-fun GHC.Classes.max () Int)
(declare-fun GHC.Types.$91$$93$ () Int)
(declare-fun GHC.Classes.$60$$61$ () Int)
(declare-fun VV$35$$35$F$35$$35$4 () Int)
(declare-fun liquid_internal_this () Int)
(declare-fun VV$35$$35$F$35$$35$11 () Int)
(declare-fun GHC.Internal.Num.$45$ () Int)
(declare-fun GHC.Internal.Num.fromInteger () Int)
(declare-fun GHC.Classes.C$58$IP () Int)
(declare-fun VV$35$$35$F$35$$35$5 () Int)
(declare-fun GHC.Types.EQ () Int)
(declare-fun n$35$$35$a2XR () Int)
(declare-fun GHC.Internal.Float.cos () Int)
(declare-fun GHC.Internal.Float.acosh () Int)
(declare-fun GHC.Internal.Real.toInteger () Int)
(declare-fun GHC.Internal.Real.$36$fIntegralInteger () Int)
(declare-fun papp3 () Int)
(declare-fun GHC.Num.Integer.IS () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL () Int)
(declare-fun autolen () Int)
(declare-fun GHC.Internal.Float.atan () Int)
(declare-fun GHC.Internal.IO.Exception.IOError () Int)
(declare-fun VV$35$$35$F$35$$35$9 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805065$35$$35$d2YV () Int)
(declare-fun GHC.Internal.Base.id () Int)
(declare-fun addrLen () Int)
(declare-fun GHC.Tuple.$40$$41$ () Int)
(declare-fun GHC.Internal.Float.exp () Int)
(declare-fun n$35$$35$a2XQ () Int)
(declare-fun GHC.Internal.Float.atanh () Int)
(declare-fun GHC.Types.True () Bool)
(declare-fun GHC.Internal.Err.error () Int)
(declare-fun GHC.Internal.Float.sinh () Int)
(declare-fun GHC.Classes.$60$ () Int)
(declare-fun head () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ () Int)
(declare-fun GHC.Internal.Float.tan () Int)
(declare-fun GHC.Internal.Real.$94$ () Int)
(declare-fun tail () Int)
(declare-fun GHC.Types.GT () Int)
(declare-fun GHC.Internal.Num.$42$ () Int)
(declare-fun VV$35$$35$F$35$$35$7 () Int)
(declare-fun GHC.Internal.Float.pi () Int)
(declare-fun GHC.Internal.Data.Either.Left () Int)
(declare-fun lqdc$35$$35$$36$select$35$$35$GHC.Internal.Maybe.Just$35$$35$1 () Int)
(declare-fun papp6 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK () Int)
(declare-fun GHC.Internal.Real.mod () Int)
(declare-fun GHC.Internal.Real.fromRational () Int)
(declare-fun GHC.Internal.Data.Tuple.fst () Int)
(declare-fun GHC.Internal.Num.$43$ () Int)
(declare-fun VV$35$$35$F$35$$35$14 () Bool)
(declare-fun GHC.Types.C$35$ () Int)
(declare-fun GHC.Internal.Stack.Types.PushCallStack () Int)
(declare-fun GHC.Internal.Float.sqrt () Int)
(declare-fun cast_as_int () Int)
(declare-fun GHC.Tuple.$40$$44$$44$$41$ () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun GHC.Types.$58$ () Int)
(declare-fun GHC.Classes.$62$$61$ () Int)
(declare-fun GHC.Types.I$35$ () Int)
(declare-fun GHC.Classes.not () Int)
(declare-fun GHC.Internal.Real.fromIntegral () Int)
(declare-fun VV$35$$35$F$35$$35$13 () Int)
(declare-fun GHC.Internal.Maybe.Nothing () Int)
(declare-fun GHC.Internal.Data.Either.Right () Int)
(declare-fun apply$35$$35$4 (Int Int) (_ BitVec 32))
(declare-fun apply$35$$35$16 (Int Str) (_ BitVec 32))
(declare-fun apply$35$$35$32 (Int (_ BitVec 64)) Str)
(declare-fun apply$35$$35$10 (Int Bool) (_ BitVec 32))
(declare-fun apply$35$$35$8 (Int Bool) Str)
(declare-fun apply$35$$35$14 (Int Str) Str)
(declare-fun apply$35$$35$21 (Int (Array Int Bool)) (Array Int Bool))
(declare-fun apply$35$$35$27 (Int (_ BitVec 32)) (Array Int Bool))
(declare-fun apply$35$$35$0 (Int Int) Int)
(declare-fun apply$35$$35$25 (Int (_ BitVec 32)) Bool)
(declare-fun apply$35$$35$31 (Int (_ BitVec 64)) Bool)
(declare-fun apply$35$$35$1 (Int Int) Bool)
(declare-fun apply$35$$35$34 (Int (_ BitVec 64)) (_ BitVec 32))
(declare-fun apply$35$$35$13 (Int Str) Bool)
(declare-fun apply$35$$35$20 (Int (Array Int Bool)) Str)
(declare-fun apply$35$$35$11 (Int Bool) (_ BitVec 64))
(declare-fun apply$35$$35$5 (Int Int) (_ BitVec 64))
(declare-fun apply$35$$35$33 (Int (_ BitVec 64)) (Array Int Bool))
(declare-fun apply$35$$35$30 (Int (_ BitVec 64)) Int)
(declare-fun apply$35$$35$24 (Int (_ BitVec 32)) Int)
(declare-fun apply$35$$35$28 (Int (_ BitVec 32)) (_ BitVec 32))
(declare-fun apply$35$$35$23 (Int (Array Int Bool)) (_ BitVec 64))
(declare-fun apply$35$$35$26 (Int (_ BitVec 32)) Str)
(declare-fun apply$35$$35$12 (Int Str) Int)
(declare-fun apply$35$$35$7 (Int Bool) Bool)
(declare-fun apply$35$$35$17 (Int Str) (_ BitVec 64))
(declare-fun apply$35$$35$15 (Int Str) (Array Int Bool))
(declare-fun apply$35$$35$18 (Int (Array Int Bool)) Int)
(declare-fun apply$35$$35$6 (Int Bool) Int)
(declare-fun apply$35$$35$9 (Int Bool) (Array Int Bool))
(declare-fun apply$35$$35$3 (Int Int) (Array Int Bool))
(declare-fun apply$35$$35$29 (Int (_ BitVec 32)) (_ BitVec 64))
(declare-fun apply$35$$35$2 (Int Int) Str)
(declare-fun apply$35$$35$22 (Int (Array Int Bool)) (_ BitVec 32))
(declare-fun apply$35$$35$35 (Int (_ BitVec 64)) (_ BitVec 64))
(declare-fun apply$35$$35$19 (Int (Array Int Bool)) Bool)
(declare-fun coerce$35$$35$4 (Int) (_ BitVec 32))
(declare-fun coerce$35$$35$16 (Str) (_ BitVec 32))
(declare-fun coerce$35$$35$32 ((_ BitVec 64)) Str)
(declare-fun coerce$35$$35$10 (Bool) (_ BitVec 32))
(declare-fun coerce$35$$35$8 (Bool) Str)
(declare-fun coerce$35$$35$14 (Str) Str)
(declare-fun coerce$35$$35$21 ((Array Int Bool)) (Array Int Bool))
(declare-fun coerce$35$$35$27 ((_ BitVec 32)) (Array Int Bool))
(declare-fun coerce$35$$35$0 (Int) Int)
(declare-fun coerce$35$$35$25 ((_ BitVec 32)) Bool)
(declare-fun coerce$35$$35$31 ((_ BitVec 64)) Bool)
(declare-fun coerce$35$$35$1 (Int) Bool)
(declare-fun coerce$35$$35$34 ((_ BitVec 64)) (_ BitVec 32))
(declare-fun coerce$35$$35$13 (Str) Bool)
(declare-fun coerce$35$$35$20 ((Array Int Bool)) Str)
(declare-fun coerce$35$$35$11 (Bool) (_ BitVec 64))
(declare-fun coerce$35$$35$5 (Int) (_ BitVec 64))
(declare-fun coerce$35$$35$33 ((_ BitVec 64)) (Array Int Bool))
(declare-fun coerce$35$$35$30 ((_ BitVec 64)) Int)
(declare-fun coerce$35$$35$24 ((_ BitVec 32)) Int)
(declare-fun coerce$35$$35$28 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun coerce$35$$35$23 ((Array Int Bool)) (_ BitVec 64))
(declare-fun coerce$35$$35$26 ((_ BitVec 32)) Str)
(declare-fun coerce$35$$35$12 (Str) Int)
(declare-fun coerce$35$$35$7 (Bool) Bool)
(declare-fun coerce$35$$35$17 (Str) (_ BitVec 64))
(declare-fun coerce$35$$35$15 (Str) (Array Int Bool))
(declare-fun coerce$35$$35$18 ((Array Int Bool)) Int)
(declare-fun coerce$35$$35$6 (Bool) Int)
(declare-fun coerce$35$$35$9 (Bool) (Array Int Bool))
(declare-fun coerce$35$$35$3 (Int) (Array Int Bool))
(declare-fun coerce$35$$35$29 ((_ BitVec 32)) (_ BitVec 64))
(declare-fun coerce$35$$35$2 (Int) Str)
(declare-fun coerce$35$$35$22 ((Array Int Bool)) (_ BitVec 32))
(declare-fun coerce$35$$35$35 ((_ BitVec 64)) (_ BitVec 64))
(declare-fun coerce$35$$35$19 ((Array Int Bool)) Bool)
(declare-fun smt_lambda$35$$35$4 (Int (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$16 (Str (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$32 ((_ BitVec 64) Str) Int)
(declare-fun smt_lambda$35$$35$10 (Bool (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$8 (Bool Str) Int)
(declare-fun smt_lambda$35$$35$14 (Str Str) Int)
(declare-fun smt_lambda$35$$35$21 ((Array Int Bool) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$27 ((_ BitVec 32) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$0 (Int Int) Int)
(declare-fun smt_lambda$35$$35$25 ((_ BitVec 32) Bool) Int)
(declare-fun smt_lambda$35$$35$31 ((_ BitVec 64) Bool) Int)
(declare-fun smt_lambda$35$$35$1 (Int Bool) Int)
(declare-fun smt_lambda$35$$35$34 ((_ BitVec 64) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$13 (Str Bool) Int)
(declare-fun smt_lambda$35$$35$20 ((Array Int Bool) Str) Int)
(declare-fun smt_lambda$35$$35$11 (Bool (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$5 (Int (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$33 ((_ BitVec 64) (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$30 ((_ BitVec 64) Int) Int)
(declare-fun smt_lambda$35$$35$24 ((_ BitVec 32) Int) Int)
(declare-fun smt_lambda$35$$35$28 ((_ BitVec 32) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$23 ((Array Int Bool) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$26 ((_ BitVec 32) Str) Int)
(declare-fun smt_lambda$35$$35$12 (Str Int) Int)
(declare-fun smt_lambda$35$$35$7 (Bool Bool) Int)
(declare-fun smt_lambda$35$$35$17 (Str (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$15 (Str (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$18 ((Array Int Bool) Int) Int)
(declare-fun smt_lambda$35$$35$6 (Bool Int) Int)
(declare-fun smt_lambda$35$$35$9 (Bool (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$3 (Int (Array Int Bool)) Int)
(declare-fun smt_lambda$35$$35$29 ((_ BitVec 32) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$2 (Int Str) Int)
(declare-fun smt_lambda$35$$35$22 ((Array Int Bool) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$35 ((_ BitVec 64) (_ BitVec 64)) Int)
(declare-fun smt_lambda$35$$35$19 ((Array Int Bool) Bool) Int)
(declare-fun lam_arg$35$$35$1$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$2$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$3$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$4$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$5$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$6$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$7$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$1$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$2$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$3$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$4$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$5$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$6$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$7$35$$35$30 () (_ BitVec 64))
(declare-fun lam_arg$35$$35$1$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$2$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$3$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$4$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$5$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$6$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$7$35$$35$24 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$1$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$2$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$3$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$4$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$5$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$6$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$7$35$$35$12 () Str)
(declare-fun lam_arg$35$$35$1$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$2$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$3$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$4$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$5$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$6$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$7$35$$35$18 () (Array Int Bool))
(declare-fun lam_arg$35$$35$1$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$2$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$3$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$4$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$5$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$6$35$$35$6 () Bool)
(declare-fun lam_arg$35$$35$7$35$$35$6 () Bool)
(assert (distinct GHC.Types.True GHC.Types.False))
(assert (distinct lit$36$htam$45$liquid$45$0.0$45$inplace lit$36$Example.BinaryGCD))

(assert (distinct GHC.Types.GT GHC.Types.EQ GHC.Types.LT))
(assert (= (strLen lit$36$Example.BinaryGCD) 17))
(assert (= (strLen lit$36$htam$45$liquid$45$0.0$45$inplace) 23))
(push 1)
(define-fun b$36$$35$$35$96 () Bool (and lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$97 () Bool (= lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP 2))
(define-fun b$36$$35$$35$98 () Bool (= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP))
(define-fun b$36$$35$$35$99 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR n$35$$35$a2XR)) (= lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$42 () Bool (not GHC.Types.False))
(define-fun b$36$$35$$35$107 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$2) 0) (= (mod VV$35$$35$F$35$$35$2 2) 1) (> VV$35$$35$F$35$$35$2 0) (<= VV$35$$35$F$35$$35$2 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$108 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$3) 0) (= (mod VV$35$$35$F$35$$35$3 2) 1) (> VV$35$$35$F$35$$35$3 0) (<= VV$35$$35$F$35$$35$3 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$109 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$4) 0) (= (mod VV$35$$35$F$35$$35$4 2) 1) (> VV$35$$35$F$35$$35$4 0) (<= VV$35$$35$F$35$$35$4 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$110 () Bool (and (= (mod lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR VV$35$$35$F$35$$35$5) 0) (= (mod VV$35$$35$F$35$$35$5 2) 1) (> VV$35$$35$F$35$$35$5 0) (<= VV$35$$35$F$35$$35$5 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR)))
(define-fun b$36$$35$$35$111 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$6 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$6 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$6 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$6 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$112 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$7 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$7 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$7 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$7 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$113 () Bool (and (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 0)) (>= VV$35$$35$F$35$$35$8 0)) (=> (and (>= n$35$$35$a2XR 0) (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1)) (<= VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (=> (>= lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ 1) (<= VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (=> (< 1 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (< VV$35$$35$F$35$$35$8 n$35$$35$a2XR)) (= VV$35$$35$F$35$$35$8 lq_anf$36$$35$$35$7205759403792805061$35$$35$d2YR) (= VV$35$$35$F$35$$35$8 (Z3_OP_DIV n$35$$35$a2XR lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ))))
(define-fun b$36$$35$$35$114 () Bool (and (= VV$35$$35$F$35$$35$9 lq_anf$36$$35$$35$7205759403792805060$35$$35$d2YQ) (= VV$35$$35$F$35$$35$9 lq_anf$36$$35$$35$7205759403792805059$35$$35$d2YP)))
(define-fun b$36$$35$$35$83 () Bool (= lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI 2))
(define-fun b$36$$35$$35$115 () Bool (and (= VV$35$$35$F$35$$35$10 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$10 0)))
(define-fun b$36$$35$$35$84 () Bool (= lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI))
(define-fun b$36$$35$$35$116 () Bool (and (= VV$35$$35$F$35$$35$11 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$11 0)))
(define-fun b$36$$35$$35$85 () Bool (and (=> (and (< 0 lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (<= 0 n$35$$35$a2XQ)) (and (< lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (<= 0 lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK))) (= lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK (mod n$35$$35$a2XQ lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ))))
(define-fun b$36$$35$$35$117 () Bool (and (= VV$35$$35$F$35$$35$12 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$12 0)))
(define-fun b$36$$35$$35$86 () Bool (= lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL 0))
(define-fun b$36$$35$$35$118 () Bool (and (= VV$35$$35$F$35$$35$13 n$35$$35$a2XR) (> VV$35$$35$F$35$$35$13 0)))
(define-fun b$36$$35$$35$87 () Bool (= lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM lq_anf$36$$35$$35$7205759403792805055$35$$35$d2YL))
(define-fun b$36$$35$$35$119 () Bool (= VV$35$$35$F$35$$35$14 (= lq_anf$36$$35$$35$7205759403792805054$35$$35$d2YK lq_anf$36$$35$$35$7205759403792805056$35$$35$d2YM)))
(define-fun b$36$$35$$35$120 () Bool (and (= VV$35$$35$F$35$$35$17 lq_anf$36$$35$$35$7205759403792805053$35$$35$d2YJ) (= VV$35$$35$F$35$$35$17 lq_anf$36$$35$$35$7205759403792805052$35$$35$d2YI)))
(define-fun b$36$$35$$35$90 () Bool (> n$35$$35$a2XR 0))
(define-fun b$36$$35$$35$91 () Bool (= lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN (= (mod n$35$$35$a2XR 2) 0)))
(define-fun b$36$$35$$35$60 () Bool GHC.Types.True)
(define-fun b$36$$35$$35$92 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$93 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$94 () Bool (and (not lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(define-fun b$36$$35$$35$95 () Bool (and (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO (= (mod n$35$$35$a2XR 2) 0)) (= lq_anf$36$$35$$35$7205759403792805058$35$$35$d2YO lq_anf$36$$35$$35$7205759403792805057$35$$35$d2YN)))
(push 1)
(push 1)
(assert (and true b$36$$35$$35$96 b$36$$35$$35$97 b$36$$35$$35$98 b$36$$35$$35$99 b$36$$35$$35$42 b$36$$35$$35$107 b$36$$35$$35$90 b$36$$35$$35$91 b$36$$35$$35$60 b$36$$35$$35$92 b$36$$35$$35$95))
(push 1)
(assert (not (= (mod VV$35$$35$F$35$$35$2 2) 1)))
(check-sat)
; SMT Says: Unsat
(pop 1)
(pop 1)
(push 1)
(assert (and true b$36$$35$$35$96 b$36$$35$$35$97 b$36$$35$$35$98 b$36$$35$$35$99 b$36$$35$$35$42 b$36$$35$$35$108 b$36$$35$$35$90 b$36$$35$$35$91 b$36$$35$$35$60 b$36$$35$$35$92 b$36$$35$$35$95))
(push 1)
(assert (not (= (mod n$35$$35$a2XR VV$35$$35$F$35$$35$3) 0)))
(check-sat)
amigalemming commented 6 days ago

Infinite loop also in z3-4.8.17.

The actual statement to be proved is the following, here expressed in Haskell/SBV:

SBV> prove $ \a b -> a.>0 .=> sMod a 2 .==0 .=> sMod b 2 ./= 0 .=> sMod (sDiv a 2) b .== 0 .=> sMod a b .== (0::SInteger)
^CInterrupted.