Skip to content

Solution soundness issue in QF_FP #10175

Description

c9a4a59

Goes back to 4.12.3 while #9953 goes back to 4.12.2. Triggers on recent Co-Pilot patch (f00cf75) for #9953

$z3 model_validate=true bug.smt2                                                
sat                                                                             
(error "line 6 column 10: an invalid model was generated")                      
$z3-4.12.3 model_validate=true bug.smt2                                         
sat                                                                             
(error "line 6 column 10: an invalid model was generated")                      
$z3-4.12.2 model_validate=true bug.smt2                                         
unsat                                                                           
$cat bug.smt2                                                                                                          
(define-fun a () (_ FloatingPoint 2 6) (_ -oo 2 6))                             
(declare-fun b () (_ FloatingPoint 2 6))        
(define-fun c () (_ FloatingPoint 2 6) ((_ to_fp 2 6) RTZ -3.25))               
(assert  (and (fp.eq b ((_ to_fp 2 6) RTZ 0.0625)) 
(fp.eq a (fp.div RTZ c b))))
(check-sat)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions