Unsat file reported as SAT

[jad-hamza]

(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (let ((g f)) (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ g r2))) g) 22) 5))))
(check-sat)

(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ f r2))) f) 22) 5)))
(check-sat)

The first file is reported as SAT (--check-models invalidates the model) while the second one (where the let g has been removed) is correctly reported as UNSAT.

The SMT file generated by Inox is:

; Options: -in -smt2
(set-option :produce-unsat-assumptions true)
(declare-fun start!1 () Bool)
(assert start!1)
(declare-fun bs!1 () Bool)
(declare-fun b!8 () Bool)
(assert (= bs!1 (and b!8 start!1)))
(declare-fun lambda!5 () Int)
(declare-fun lambda!4 () Int)
(assert (=> bs!1 (not (= lambda!5 lambda!4))))
(assert (=> b!8 true))
(declare-fun order!1 () Int)
(declare-fun dynLambda!0 (Int Int) Int)
(assert (=> b!8 (< (dynLambda!0 order!1 lambda!4) (dynLambda!0 order!1 lambda!5))))
(declare-fun c!4 () Bool)
(assert (=> start!1 (= c!4 true)))
(declare-fun e!5 () Int)
(declare-fun dynLambda!1 (Int Int) Int)
(assert (=> start!1 (not (= (dynLambda!1 e!5 22) 5))))
(assert (=> b!8 (= e!5 lambda!5)))
(declare-fun b!9 () Bool)
(assert (=> b!9 (= e!5 lambda!4)))
(assert (= (and start!1 c!4) b!8))
(assert (= (and start!1 (not c!4)) b!9))
(declare-fun b_lambda!1 () Bool)
(assert (=> (not b_lambda!1) (not start!1)))
(declare-fun m!1 () Bool)
(assert (=> start!1 m!1))
(check-sat (not b_lambda!1))
(check-sat)
(get-model)
(declare-fun b_lambda!3 () Bool)
(assert (= b_lambda!1 (or start!1 b_lambda!3)))
(declare-fun bs!2 () Bool)
(declare-fun d!1 () Bool)
(assert (= bs!2 (and d!1 start!1)))
(assert (=> bs!2 (= (dynLambda!1 lambda!4 22) 0)))
(assert (=> start!1 d!1))
(check-sat (not b_lambda!3))
(get-model)

The variable b_lambda!3 from the end only appears in the assertion (= b_lambda!1 (or start!1 b_lambda!3)), and is unconstrained because start!1 must be true.

Can this be due to #105 (which touched let's)?

[samarion]

Urgh, this seems to be an issue with lambda pointers, which are fairly complicated...

I believe the simplest fix is to remove the two Equals cases in the lambdaPointers function.

In order to preserve the optimization for the most common case, we can add an other method

def resultPointers(encoder: Expr => Encoded)(expr: Expr): Map[Encoded, Encoded] = {
  val pointers = expr match {
    case Equals(v @ (_: Variable | _: FunctionInvocation | _: Application), e) => collectSelectors(e, v).toMap
    case Equals(e, v @ (_: Variable | _: FunctionInvocation | _: Application)) => collectSelectors(e, v).toMap
    case _ => Map.empty[Expr, Variable]
  }

  pointers.map(p => encoder(p._1) -> encoder(p._2))
}

and call it inside encode (right before extending the clauses set):

for (e <- guardedExprs.getOrElse(pv, Set.empty)) {
  pointers ++= resultPointers(encoder)(e)
}

[jad-hamza]

Thanks! Fixed in #135