Unsoundness bug with smt2 file over arctan2 function.

[KJongUk]

With the following input, and precision=0.001 :

(set-logic QF_NRA)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun s1 () Real [1.0,4.0])
(declare-fun s2 () Real [1.0,4.0])
(assert (and  
        (= x 3)  
        (= (+ s1 (sqrt s2)) 4)  
        (= z (arctan2 x y))  
        (< 0.64350 z)  
        (< z 0.64351)))
(check-sat)
(exit)

dReal(v.4.21.06.2) returns unsat. but I think this formula is sat when x = 3, s1 = 2 , s2 = 4, y = 4, z = 0.643501109. (setup : Ubuntu 18.04) I have seen this happen with unbound value of arctan2's denominator.

[soonho-tri]

Thanks for the report. I'll check it.

[soonho-tri]

A smaller example:

(set-logic QF_NRA)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (= z (arctan2 3 y)))
(check-sat)
(exit)

Trace:

[trace] [20210802 08:12:33.789643] ContractorIbexFwdbwd::Prune
[trace] [20210802 08:12:33.789653] CTC = (z-atan2(3,y))=0
[trace] [20210802 08:12:33.789662] F = (z == atan2(3, y))
[debug] [20210802 08:12:33.789719] ContractorStatus::AddUsedConstraint((z == atan2(3, y))) box is empty? true
[debug] [20210802 08:12:33.789733] ContractorStatus::AddUnsatWitness(y)
[debug] [20210802 08:12:33.789740] ContractorStatus::AddUnsatWitness(z)
[trace] [20210802 08:12:33.789759] Changed
y : [ ENTIRE ] -> [ empty ]

[trace] [20210802 08:12:33.789770] IcpSeq::CheckSat() After pruning, the current box =
y : [ empty ]
z : [ ENTIRE ]
[debug] [20210802 08:12:33.789775] IcpSeq::CheckSat() Box is empty after pruning
[debug] [20210802 08:12:33.789778] IcpSeq::CheckSat() No solution
[debug] [20210802 08:12:33.789800] ContextImpl::CheckSatCore() - Theroy Check = UNSAT
[debug] [20210802 08:12:33.789808] ContextImpl::CheckSatCore() - size of explanation = 1 - stack size = 1
[trace] [20210802 08:12:33.789833] ContextImpl::CheckSatCore: Stack (z == atan2(3, y))
[trace] [20210802 08:12:33.789844] ContextImpl::CheckSatCore: Explanation (z == atan2(3, y))
[debug] [20210802 08:12:33.789854] SatSolver::CheckSat(#vars = 1, #clauses = 2)
[debug] [20210802 08:12:33.789864] SatSolver::CheckSat() No solution.
[debug] [20210802 08:12:33.789868] ContextImpl::CheckSatCore() - Sat Check = UNSAT

[soonho-tri]

FTR, this is from IBEX. I'm checking newer versions if I can reproduce it.

[KJongUk]

Thanks for taking the time.

[soonhokong]

@KJongUk , can you create a small reproducible example only using IBEX? Then I'd open an issue there.